{-|
Copyright  :  (C) 2015-2016, University of Twente
License    :  BSD2 (see the file LICENSE)
Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>

To use the plugin, add the

@
{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}
@

pragma to the header of your file

-}

{-# LANGUAGE CPP           #-}
{-# LANGUAGE TupleSections #-}

{-# OPTIONS_HADDOCK show-extensions #-}

module GHC.TypeLits.Extra.Solver
  ( plugin )
where

-- external
import Control.Monad.Trans.Maybe (MaybeT (..))
import Data.Either               (lefts)
import Data.Maybe                (catMaybes)
import GHC.TcPluginM.Extra       (evByFiat, lookupModule, lookupName,
                                  tracePlugin)

-- GHC API
import FastString (fsLit)
import Module     (mkModuleName)
import OccName    (mkTcOcc)
import Outputable (Outputable (..), (<+>), ($$), text)
import Plugins    (Plugin (..), defaultPlugin)
#if MIN_VERSION_ghc(8,6,0)
import Plugins    (purePlugin)
#endif
import TcEvidence (EvTerm)
import TcPluginM  (TcPluginM, tcLookupTyCon, tcPluginTrace)
import TcRnTypes  (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvPred,
                   isWantedCt)
import TcType      (typeKind)
import Type       (EqRel (NomEq), Kind, PredTree (EqPred), classifyPredType,
                   eqType)
import TyCoRep    (Type (..))
import TysWiredIn (typeNatKind, promotedTrueDataCon, promotedFalseDataCon)
import TcTypeNats (typeNatLeqTyCon)
#if MIN_VERSION_ghc(8,4,0)
import GHC.TcPluginM.Extra (flattenGivens)
import TcTypeNats (typeNatTyCons)
#else
import TcPluginM  (zonkCt)
import Control.Monad ((<=<))
#endif

-- internal
import GHC.TypeLits.Extra.Solver.Operations
import GHC.TypeLits.Extra.Solver.Unify

-- | A solver implement as a type-checker plugin for:
--
--     * 'Div': type-level 'div'
--
--     * 'Mod': type-level 'mod'
--
--     * 'FLog': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
--       .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"
--
--     * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
--       .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"
--
--     * 'Log': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
--        where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@"
--
--     * 'GCD': a type-level 'gcd'
--
--     * 'LCM': a type-level 'lcm'
--
-- To use the plugin, add
--
-- @
-- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}
-- @
--
-- To the header of your file.
plugin :: Plugin
plugin :: Plugin
plugin
  = Plugin
defaultPlugin
  { tcPlugin :: TcPlugin
tcPlugin = Maybe TcPlugin -> TcPlugin
forall a b. a -> b -> a
const (Maybe TcPlugin -> TcPlugin) -> Maybe TcPlugin -> TcPlugin
forall a b. (a -> b) -> a -> b
$ TcPlugin -> Maybe TcPlugin
forall a. a -> Maybe a
Just TcPlugin
normalisePlugin
#if MIN_VERSION_ghc(8,6,0)
  , pluginRecompile :: [CommandLineOption] -> IO PluginRecompile
pluginRecompile = [CommandLineOption] -> IO PluginRecompile
purePlugin
#endif
  }

normalisePlugin :: TcPlugin
normalisePlugin :: TcPlugin
normalisePlugin = CommandLineOption -> TcPlugin -> TcPlugin
tracePlugin "ghc-typelits-extra"
  TcPlugin :: forall s.
TcPluginM s
-> (s -> TcPluginSolver) -> (s -> TcPluginM ()) -> TcPlugin
TcPlugin { tcPluginInit :: TcPluginM ExtraDefs
tcPluginInit  = TcPluginM ExtraDefs
lookupExtraDefs
           , tcPluginSolve :: ExtraDefs -> TcPluginSolver
tcPluginSolve = ExtraDefs -> TcPluginSolver
decideEqualSOP
           , tcPluginStop :: ExtraDefs -> TcPluginM ()
tcPluginStop  = TcPluginM () -> ExtraDefs -> TcPluginM ()
forall a b. a -> b -> a
const (() -> TcPluginM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
           }

decideEqualSOP :: ExtraDefs -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
decideEqualSOP :: ExtraDefs -> TcPluginSolver
decideEqualSOP _    _givens :: [Ct]
_givens _deriveds :: [Ct]
_deriveds []      = TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk [] [])
decideEqualSOP defs :: ExtraDefs
defs givens :: [Ct]
givens  _deriveds :: [Ct]
_deriveds wanteds :: [Ct]
wanteds = do
  -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out
  let wanteds' :: [Ct]
wanteds' = (Ct -> Bool) -> [Ct] -> [Ct]
forall a. (a -> Bool) -> [a] -> [a]
filter Ct -> Bool
isWantedCt [Ct]
wanteds
  [Either NatEquality NatInEquality]
unit_wanteds <- [Maybe (Either NatEquality NatInEquality)]
-> [Either NatEquality NatInEquality]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Either NatEquality NatInEquality)]
 -> [Either NatEquality NatInEquality])
-> TcPluginM [Maybe (Either NatEquality NatInEquality)]
-> TcPluginM [Either NatEquality NatInEquality]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ct -> TcPluginM (Maybe (Either NatEquality NatInEquality)))
-> [Ct] -> TcPluginM [Maybe (Either NatEquality NatInEquality)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (MaybeT TcPluginM (Either NatEquality NatInEquality)
-> TcPluginM (Maybe (Either NatEquality NatInEquality))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT TcPluginM (Either NatEquality NatInEquality)
 -> TcPluginM (Maybe (Either NatEquality NatInEquality)))
-> (Ct -> MaybeT TcPluginM (Either NatEquality NatInEquality))
-> Ct
-> TcPluginM (Maybe (Either NatEquality NatInEquality))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtraDefs
-> Ct -> MaybeT TcPluginM (Either NatEquality NatInEquality)
toNatEquality ExtraDefs
defs) [Ct]
wanteds'
  case [Either NatEquality NatInEquality]
unit_wanteds of
    [] -> TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk [] [])
    _  -> do
#if MIN_VERSION_ghc(8,4,0)
      [Either NatEquality NatInEquality]
unit_givens <- [Maybe (Either NatEquality NatInEquality)]
-> [Either NatEquality NatInEquality]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Either NatEquality NatInEquality)]
 -> [Either NatEquality NatInEquality])
-> TcPluginM [Maybe (Either NatEquality NatInEquality)]
-> TcPluginM [Either NatEquality NatInEquality]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ct -> TcPluginM (Maybe (Either NatEquality NatInEquality)))
-> [Ct] -> TcPluginM [Maybe (Either NatEquality NatInEquality)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (MaybeT TcPluginM (Either NatEquality NatInEquality)
-> TcPluginM (Maybe (Either NatEquality NatInEquality))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT TcPluginM (Either NatEquality NatInEquality)
 -> TcPluginM (Maybe (Either NatEquality NatInEquality)))
-> (Ct -> MaybeT TcPluginM (Either NatEquality NatInEquality))
-> Ct
-> TcPluginM (Maybe (Either NatEquality NatInEquality))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtraDefs
-> Ct -> MaybeT TcPluginM (Either NatEquality NatInEquality)
toNatEquality ExtraDefs
defs) ([Ct]
givens [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct] -> [Ct]
flattenGivens [Ct]
givens)
#else
      unit_givens <- catMaybes <$> mapM ((runMaybeT . toNatEquality defs) <=< zonkCt) givens
#endif
      SimplifyResult
sr <- [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
simplifyExtra ([Either NatEquality NatInEquality]
unit_givens [Either NatEquality NatInEquality]
-> [Either NatEquality NatInEquality]
-> [Either NatEquality NatInEquality]
forall a. [a] -> [a] -> [a]
++ [Either NatEquality NatInEquality]
unit_wanteds)
      CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace "normalised" (SimplifyResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr SimplifyResult
sr)
      case SimplifyResult
sr of
        Simplified evs :: [(EvTerm, Ct)]
evs -> TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk (((EvTerm, Ct) -> Bool) -> [(EvTerm, Ct)] -> [(EvTerm, Ct)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Ct -> Bool
isWantedCt (Ct -> Bool) -> ((EvTerm, Ct) -> Ct) -> (EvTerm, Ct) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EvTerm, Ct) -> Ct
forall a b. (a, b) -> b
snd) [(EvTerm, Ct)]
evs) [])
        Impossible eq :: Either NatEquality NatInEquality
eq  -> TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([Ct] -> TcPluginResult
TcPluginContradiction [Either NatEquality NatInEquality -> Ct
fromNatEquality Either NatEquality NatInEquality
eq])

type NatEquality   = (Ct,ExtraOp,ExtraOp)
type NatInEquality = (Ct,ExtraOp,ExtraOp,Bool)

data SimplifyResult
  = Simplified [(EvTerm,Ct)]
  | Impossible (Either NatEquality NatInEquality)

instance Outputable SimplifyResult where
  ppr :: SimplifyResult -> SDoc
ppr (Simplified evs :: [(EvTerm, Ct)]
evs) = CommandLineOption -> SDoc
text "Simplified" SDoc -> SDoc -> SDoc
$$ [(EvTerm, Ct)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(EvTerm, Ct)]
evs
  ppr (Impossible eq :: Either NatEquality NatInEquality
eq)  = CommandLineOption -> SDoc
text "Impossible" SDoc -> SDoc -> SDoc
<+> Either NatEquality NatInEquality -> SDoc
forall a. Outputable a => a -> SDoc
ppr Either NatEquality NatInEquality
eq

simplifyExtra :: [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
simplifyExtra :: [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
simplifyExtra eqs :: [Either NatEquality NatInEquality]
eqs = CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace "simplifyExtra" ([Either NatEquality NatInEquality] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Either NatEquality NatInEquality]
eqs) TcPluginM ()
-> TcPluginM SimplifyResult -> TcPluginM SimplifyResult
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Maybe (EvTerm, Ct)]
-> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
simples [] [Either NatEquality NatInEquality]
eqs
  where
    simples :: [Maybe (EvTerm, Ct)] -> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
    simples :: [Maybe (EvTerm, Ct)]
-> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
simples evs :: [Maybe (EvTerm, Ct)]
evs [] = SimplifyResult -> TcPluginM SimplifyResult
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> SimplifyResult
Simplified ([Maybe (EvTerm, Ct)] -> [(EvTerm, Ct)]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (EvTerm, Ct)]
evs))
    simples evs :: [Maybe (EvTerm, Ct)]
evs (eq :: Either NatEquality NatInEquality
eq@(Left (ct :: Ct
ct,u :: ExtraOp
u,v :: ExtraOp
v)):eqs' :: [Either NatEquality NatInEquality]
eqs') = do
      UnifyResult
ur <- Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult
unifyExtra Ct
ct ExtraOp
u ExtraOp
v
      CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace "unifyExtra result" (UnifyResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr UnifyResult
ur)
      case UnifyResult
ur of
        Win  -> [Maybe (EvTerm, Ct)]
-> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
simples (((,) (EvTerm -> Ct -> (EvTerm, Ct))
-> Maybe EvTerm -> Maybe (Ct -> (EvTerm, Ct))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct -> Maybe EvTerm
evMagic Ct
ct Maybe (Ct -> (EvTerm, Ct)) -> Maybe Ct -> Maybe (EvTerm, Ct)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Ct -> Maybe Ct
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ct
ct)Maybe (EvTerm, Ct) -> [Maybe (EvTerm, Ct)] -> [Maybe (EvTerm, Ct)]
forall a. a -> [a] -> [a]
:[Maybe (EvTerm, Ct)]
evs) [Either NatEquality NatInEquality]
eqs'
        Lose -> if [Maybe (EvTerm, Ct)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Maybe (EvTerm, Ct)]
evs Bool -> Bool -> Bool
&& [Either NatEquality NatInEquality] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Either NatEquality NatInEquality]
eqs'
                   then SimplifyResult -> TcPluginM SimplifyResult
forall (m :: * -> *) a. Monad m => a -> m a
return  (Either NatEquality NatInEquality -> SimplifyResult
Impossible Either NatEquality NatInEquality
eq)
                   else [Maybe (EvTerm, Ct)]
-> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
simples [Maybe (EvTerm, Ct)]
evs [Either NatEquality NatInEquality]
eqs'
        Draw -> [Maybe (EvTerm, Ct)]
-> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
simples [Maybe (EvTerm, Ct)]
evs [Either NatEquality NatInEquality]
eqs'
    simples evs :: [Maybe (EvTerm, Ct)]
evs (eq :: Either NatEquality NatInEquality
eq@(Right (ct :: Ct
ct,u :: ExtraOp
u,v :: ExtraOp
v,b :: Bool
b)):eqs' :: [Either NatEquality NatInEquality]
eqs') = do
      CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace "unifyExtra leq result" ((ExtraOp, ExtraOp, Bool) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (ExtraOp
u,ExtraOp
v,Bool
b))
      case (ExtraOp
u,ExtraOp
v) of
        (I i :: Integer
i,I j :: Integer
j)
          | (Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
j) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b -> [Maybe (EvTerm, Ct)]
-> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
simples (((,) (EvTerm -> Ct -> (EvTerm, Ct))
-> Maybe EvTerm -> Maybe (Ct -> (EvTerm, Ct))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct -> Maybe EvTerm
evMagic Ct
ct Maybe (Ct -> (EvTerm, Ct)) -> Maybe Ct -> Maybe (EvTerm, Ct)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Ct -> Maybe Ct
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ct
ct)Maybe (EvTerm, Ct) -> [Maybe (EvTerm, Ct)] -> [Maybe (EvTerm, Ct)]
forall a. a -> [a] -> [a]
:[Maybe (EvTerm, Ct)]
evs) [Either NatEquality NatInEquality]
eqs'
          | Bool
otherwise     -> SimplifyResult -> TcPluginM SimplifyResult
forall (m :: * -> *) a. Monad m => a -> m a
return  (Either NatEquality NatInEquality -> SimplifyResult
Impossible Either NatEquality NatInEquality
eq)
        (p :: ExtraOp
p, Max x :: ExtraOp
x y :: ExtraOp
y)
          | Bool
b Bool -> Bool -> Bool
&& (ExtraOp
p ExtraOp -> ExtraOp -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraOp
x Bool -> Bool -> Bool
|| ExtraOp
p ExtraOp -> ExtraOp -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraOp
y) -> [Maybe (EvTerm, Ct)]
-> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
simples (((,) (EvTerm -> Ct -> (EvTerm, Ct))
-> Maybe EvTerm -> Maybe (Ct -> (EvTerm, Ct))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ct -> Maybe EvTerm
evMagic Ct
ct Maybe (Ct -> (EvTerm, Ct)) -> Maybe Ct -> Maybe (EvTerm, Ct)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Ct -> Maybe Ct
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ct
ct)Maybe (EvTerm, Ct) -> [Maybe (EvTerm, Ct)] -> [Maybe (EvTerm, Ct)]
forall a. a -> [a] -> [a]
:[Maybe (EvTerm, Ct)]
evs) [Either NatEquality NatInEquality]
eqs'

        -- transform:  q ~ Max x y => (p <=? q ~ True)
        -- to:         (p <=? Max x y) ~ True
        -- and try to solve that along with the rest of the eqs'
        (p :: ExtraOp
p, q :: ExtraOp
q@(V _))
          | Bool
b -> case ExtraOp -> [Either NatEquality NatInEquality] -> Maybe ExtraOp
findMax ExtraOp
q [Either NatEquality NatInEquality]
eqs of
                   Just m :: ExtraOp
m  -> [Maybe (EvTerm, Ct)]
-> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
simples [Maybe (EvTerm, Ct)]
evs ((NatInEquality -> Either NatEquality NatInEquality
forall a b. b -> Either a b
Right (Ct
ct,ExtraOp
p,ExtraOp
m,Bool
b))Either NatEquality NatInEquality
-> [Either NatEquality NatInEquality]
-> [Either NatEquality NatInEquality]
forall a. a -> [a] -> [a]
:[Either NatEquality NatInEquality]
eqs')
                   Nothing -> [Maybe (EvTerm, Ct)]
-> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
simples [Maybe (EvTerm, Ct)]
evs [Either NatEquality NatInEquality]
eqs'
        _ -> [Maybe (EvTerm, Ct)]
-> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
simples [Maybe (EvTerm, Ct)]
evs [Either NatEquality NatInEquality]
eqs'

    -- look for given constraint with the form: c ~ Max x y
    findMax :: ExtraOp -> [Either NatEquality NatInEquality] -> Maybe ExtraOp
    findMax :: ExtraOp -> [Either NatEquality NatInEquality] -> Maybe ExtraOp
findMax c :: ExtraOp
c = [NatEquality] -> Maybe ExtraOp
go ([NatEquality] -> Maybe ExtraOp)
-> ([Either NatEquality NatInEquality] -> [NatEquality])
-> [Either NatEquality NatInEquality]
-> Maybe ExtraOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Either NatEquality NatInEquality] -> [NatEquality]
forall a b. [Either a b] -> [a]
lefts
      where
        go :: [NatEquality] -> Maybe ExtraOp
go [] = Maybe ExtraOp
forall a. Maybe a
Nothing
        go ((ct :: Ct
ct, a :: ExtraOp
a,b :: ExtraOp
b@(Max _ _)) :_)
          | ExtraOp
c ExtraOp -> ExtraOp -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraOp
a Bool -> Bool -> Bool
&& Bool -> Bool
not (Ct -> Bool
isWantedCt Ct
ct)
            = ExtraOp -> Maybe ExtraOp
forall a. a -> Maybe a
Just ExtraOp
b
        go ((ct :: Ct
ct, a :: ExtraOp
a@(Max _ _),b :: ExtraOp
b) :_)
          | ExtraOp
c ExtraOp -> ExtraOp -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraOp
b Bool -> Bool -> Bool
&& Bool -> Bool
not (Ct -> Bool
isWantedCt Ct
ct)
            = ExtraOp -> Maybe ExtraOp
forall a. a -> Maybe a
Just ExtraOp
a
        go (_:rest :: [NatEquality]
rest) = [NatEquality] -> Maybe ExtraOp
go [NatEquality]
rest


-- Extract the Nat equality constraints
toNatEquality :: ExtraDefs -> Ct -> MaybeT TcPluginM (Either NatEquality NatInEquality)
toNatEquality :: ExtraDefs
-> Ct -> MaybeT TcPluginM (Either NatEquality NatInEquality)
toNatEquality defs :: ExtraDefs
defs ct :: Ct
ct = case PredType -> PredTree
classifyPredType (PredType -> PredTree) -> PredType -> PredTree
forall a b. (a -> b) -> a -> b
$ CtEvidence -> PredType
ctEvPred (CtEvidence -> PredType) -> CtEvidence -> PredType
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct of
    EqPred NomEq t1 :: PredType
t1 t2 :: PredType
t2
      | PredType -> Bool
isNatKind (HasDebugCallStack => PredType -> PredType
PredType -> PredType
typeKind PredType
t1) Bool -> Bool -> Bool
|| PredType -> Bool
isNatKind (HasDebugCallStack => PredType -> PredType
PredType -> PredType
typeKind PredType
t2)
      -> NatEquality -> Either NatEquality NatInEquality
forall a b. a -> Either a b
Left (NatEquality -> Either NatEquality NatInEquality)
-> MaybeT TcPluginM NatEquality
-> MaybeT TcPluginM (Either NatEquality NatInEquality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Ct
ct,,) (ExtraOp -> ExtraOp -> NatEquality)
-> MaybeT TcPluginM ExtraOp
-> MaybeT TcPluginM (ExtraOp -> NatEquality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExtraDefs -> PredType -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs PredType
t1 MaybeT TcPluginM (ExtraOp -> NatEquality)
-> MaybeT TcPluginM ExtraOp -> MaybeT TcPluginM NatEquality
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExtraDefs -> PredType -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs PredType
t2)
      | TyConApp tc :: TyCon
tc [x :: PredType
x,y :: PredType
y] <- PredType
t1
      , TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatLeqTyCon
      , TyConApp tc' :: TyCon
tc' [] <- PredType
t2
      -> if TyCon
tc' TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedTrueDataCon
            then NatInEquality -> Either NatEquality NatInEquality
forall a b. b -> Either a b
Right (NatInEquality -> Either NatEquality NatInEquality)
-> MaybeT TcPluginM NatInEquality
-> MaybeT TcPluginM (Either NatEquality NatInEquality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Ct
ct,,,Bool
True) (ExtraOp -> ExtraOp -> NatInEquality)
-> MaybeT TcPluginM ExtraOp
-> MaybeT TcPluginM (ExtraOp -> NatInEquality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExtraDefs -> PredType -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs PredType
x MaybeT TcPluginM (ExtraOp -> NatInEquality)
-> MaybeT TcPluginM ExtraOp -> MaybeT TcPluginM NatInEquality
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExtraDefs -> PredType -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs PredType
y)
            else if TyCon
tc' TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedFalseDataCon
                 then NatInEquality -> Either NatEquality NatInEquality
forall a b. b -> Either a b
Right (NatInEquality -> Either NatEquality NatInEquality)
-> MaybeT TcPluginM NatInEquality
-> MaybeT TcPluginM (Either NatEquality NatInEquality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Ct
ct,,,Bool
False) (ExtraOp -> ExtraOp -> NatInEquality)
-> MaybeT TcPluginM ExtraOp
-> MaybeT TcPluginM (ExtraOp -> NatInEquality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExtraDefs -> PredType -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs PredType
x MaybeT TcPluginM (ExtraOp -> NatInEquality)
-> MaybeT TcPluginM ExtraOp -> MaybeT TcPluginM NatInEquality
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExtraDefs -> PredType -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs PredType
y)
                 else CommandLineOption
-> MaybeT TcPluginM (Either NatEquality NatInEquality)
forall (m :: * -> *) a. MonadFail m => CommandLineOption -> m a
fail "Nothing"
    _ -> CommandLineOption
-> MaybeT TcPluginM (Either NatEquality NatInEquality)
forall (m :: * -> *) a. MonadFail m => CommandLineOption -> m a
fail "Nothing"
  where
    isNatKind :: Kind -> Bool
    isNatKind :: PredType -> Bool
isNatKind = (PredType -> PredType -> Bool
`eqType` PredType
typeNatKind)

fromNatEquality :: Either NatEquality NatInEquality -> Ct
fromNatEquality :: Either NatEquality NatInEquality -> Ct
fromNatEquality (Left (ct :: Ct
ct, _, _))  = Ct
ct
fromNatEquality (Right (ct :: Ct
ct,_,_,_)) = Ct
ct

lookupExtraDefs :: TcPluginM ExtraDefs
lookupExtraDefs :: TcPluginM ExtraDefs
lookupExtraDefs = do
    Module
md <- ModuleName -> FastString -> TcPluginM Module
lookupModule ModuleName
myModule FastString
myPackage
    TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> ExtraDefs
ExtraDefs (TyCon
 -> TyCon
 -> TyCon
 -> TyCon
 -> TyCon
 -> TyCon
 -> TyCon
 -> TyCon
 -> TyCon
 -> ExtraDefs)
-> TcPluginM TyCon
-> TcPluginM
     (TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> TyCon
      -> ExtraDefs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Module -> CommandLineOption -> TcPluginM TyCon
look Module
md "Max"
              TcPluginM
  (TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> TyCon
   -> ExtraDefs)
-> TcPluginM TyCon
-> TcPluginM
     (TyCon
      -> TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Module -> CommandLineOption -> TcPluginM TyCon
look Module
md "Min"
#if MIN_VERSION_ghc(8,4,0)
              TcPluginM
  (TyCon
   -> TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
-> TcPluginM TyCon
-> TcPluginM
     (TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TyCon -> TcPluginM TyCon
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TyCon]
typeNatTyCons [TyCon] -> Int -> TyCon
forall a. [a] -> Int -> a
!! 5)
              TcPluginM
  (TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
-> TcPluginM TyCon
-> TcPluginM
     (TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TyCon -> TcPluginM TyCon
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TyCon]
typeNatTyCons [TyCon] -> Int -> TyCon
forall a. [a] -> Int -> a
!! 6)
#else
              <*> look md "Div"
              <*> look md "Mod"
#endif
              TcPluginM (TyCon -> TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
-> TcPluginM TyCon
-> TcPluginM (TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Module -> CommandLineOption -> TcPluginM TyCon
look Module
md "FLog"
              TcPluginM (TyCon -> TyCon -> TyCon -> TyCon -> ExtraDefs)
-> TcPluginM TyCon
-> TcPluginM (TyCon -> TyCon -> TyCon -> ExtraDefs)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Module -> CommandLineOption -> TcPluginM TyCon
look Module
md "CLog"
              TcPluginM (TyCon -> TyCon -> TyCon -> ExtraDefs)
-> TcPluginM TyCon -> TcPluginM (TyCon -> TyCon -> ExtraDefs)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Module -> CommandLineOption -> TcPluginM TyCon
look Module
md "Log"
              TcPluginM (TyCon -> TyCon -> ExtraDefs)
-> TcPluginM TyCon -> TcPluginM (TyCon -> ExtraDefs)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Module -> CommandLineOption -> TcPluginM TyCon
look Module
md "GCD"
              TcPluginM (TyCon -> ExtraDefs)
-> TcPluginM TyCon -> TcPluginM ExtraDefs
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Module -> CommandLineOption -> TcPluginM TyCon
look Module
md "LCM"
  where
    look :: Module -> CommandLineOption -> TcPluginM TyCon
look md :: Module
md s :: CommandLineOption
s = Name -> TcPluginM TyCon
tcLookupTyCon (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupName Module
md (CommandLineOption -> OccName
mkTcOcc CommandLineOption
s)
    myModule :: ModuleName
myModule  = CommandLineOption -> ModuleName
mkModuleName "GHC.TypeLits.Extra"
    myPackage :: FastString
myPackage = CommandLineOption -> FastString
fsLit "ghc-typelits-extra"

-- Utils
evMagic :: Ct -> Maybe EvTerm
evMagic :: Ct -> Maybe EvTerm
evMagic ct :: Ct
ct = case PredType -> PredTree
classifyPredType (PredType -> PredTree) -> PredType -> PredTree
forall a b. (a -> b) -> a -> b
$ CtEvidence -> PredType
ctEvPred (CtEvidence -> PredType) -> CtEvidence -> PredType
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct of
    EqPred NomEq t1 :: PredType
t1 t2 :: PredType
t2 -> EvTerm -> Maybe EvTerm
forall a. a -> Maybe a
Just (CommandLineOption -> PredType -> PredType -> EvTerm
evByFiat "ghc-typelits-extra" PredType
t1 PredType
t2)
    _                  -> Maybe EvTerm
forall a. Maybe a
Nothing