{-|
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 DataKinds #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TemplateHaskellQuotes #-}

{-# OPTIONS_HADDOCK show-extensions #-}

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

-- external
import Control.Monad.Trans.Maybe (MaybeT (..))
import Data.Maybe (catMaybes)

-- ghc-tcplugin-api
import GHC.TcPlugin.API
import GHC.TcPlugin.API.TyConSubst

-- GHC API
import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon)
import GHC.Core.DataCon (dataConWrapId)
import GHC.Core.TyCo.Rep (Type (..), TyLit (..))
import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin)
import GHC.Tc.Types.Constraint (isWantedCt)
import GHC.Utils.Outputable ((<+>), ($$), text, vcat)

-- ghc-typelits-natnormalise
import GHC.TypeLits.Normalise.Compat

-- internal
import GHC.TypeLits.Extra.Solver.Compat
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/base-4.17.0.0/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/base-4.17.0.0/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/base-4.17.0.0/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 = const (pure (mkTcPlugin normalisePlugin))
  , pluginRecompile = purePlugin
  }

normalisePlugin :: TcPlugin
normalisePlugin :: TcPlugin
normalisePlugin =
  TcPlugin { tcPluginInit :: TcPluginM 'Init ExtraDefs
tcPluginInit    = TcPluginM 'Init ExtraDefs
lookupExtraDefs
           , tcPluginSolve :: ExtraDefs -> TcPluginSolver
tcPluginSolve   = ExtraDefs -> TcPluginSolver
decideEqualSOP
           , tcPluginRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter
tcPluginRewrite = ExtraDefs -> UniqFM TyCon TcPluginRewriter
extraRewrite
           , tcPluginStop :: ExtraDefs -> TcPluginM 'Stop ()
tcPluginStop    = TcPluginM 'Stop () -> ExtraDefs -> TcPluginM 'Stop ()
forall a b. a -> b -> a
const (() -> TcPluginM 'Stop ()
forall a. a -> TcPluginM 'Stop a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
           }

extraRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter
extraRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter
extraRewrite ExtraDefs
defs = [(TyCon, TcPluginRewriter)] -> UniqFM TyCon TcPluginRewriter
forall key elt. Uniquable key => [(key, elt)] -> UniqFM key elt
listToUFM
  [ (ExtraDefs -> TyCon
gcdTyCon ExtraDefs
defs, TcPluginRewriter
forall {f :: * -> *} {p}.
Applicative f =>
p -> [Type] -> f TcPluginRewriteResult
gcdRewrite)
  , (ExtraDefs -> TyCon
lcmTyCon ExtraDefs
defs, TcPluginRewriter
forall {f :: * -> *} {p}.
Applicative f =>
p -> [Type] -> f TcPluginRewriteResult
lcmRewrite)
  ]
  where
    gcdRewrite :: p -> [Type] -> f TcPluginRewriteResult
gcdRewrite p
_ args :: [Type]
args@[LitTy (NumTyLit Integer
i), LitTy (NumTyLit Integer
j)] = TcPluginRewriteResult -> f TcPluginRewriteResult
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TcPluginRewriteResult -> f TcPluginRewriteResult)
-> TcPluginRewriteResult -> f TcPluginRewriteResult
forall a b. (a -> b) -> a -> b
$
      Reduction -> [Ct] -> TcPluginRewriteResult
TcPluginRewriteTo (TyCon -> [Type] -> Type -> Reduction
reduce (ExtraDefs -> TyCon
gcdTyCon ExtraDefs
defs) [Type]
args (TyLit -> Type
LitTy (Integer -> TyLit
NumTyLit (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`gcd` Integer
j)))) []
    gcdRewrite p
_ [Type]
_ = TcPluginRewriteResult -> f TcPluginRewriteResult
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TcPluginRewriteResult
TcPluginNoRewrite

    lcmRewrite :: p -> [Type] -> f TcPluginRewriteResult
lcmRewrite p
_ args :: [Type]
args@[LitTy (NumTyLit Integer
i), LitTy (NumTyLit Integer
j)] = TcPluginRewriteResult -> f TcPluginRewriteResult
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TcPluginRewriteResult -> f TcPluginRewriteResult)
-> TcPluginRewriteResult -> f TcPluginRewriteResult
forall a b. (a -> b) -> a -> b
$
      Reduction -> [Ct] -> TcPluginRewriteResult
TcPluginRewriteTo (TyCon -> [Type] -> Type -> Reduction
reduce (ExtraDefs -> TyCon
lcmTyCon ExtraDefs
defs) [Type]
args (TyLit -> Type
LitTy (Integer -> TyLit
NumTyLit (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`lcm` Integer
j)))) []
    lcmRewrite p
_ [Type]
_ = TcPluginRewriteResult -> f TcPluginRewriteResult
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TcPluginRewriteResult
TcPluginNoRewrite

    reduce :: TyCon -> [Type] -> Type -> Reduction
reduce TyCon
tc [Type]
args Type
res = Coercion -> Type -> Reduction
Reduction Coercion
co Type
res
     where
      co :: Coercion
co = CommandLineOption -> Role -> [Coercion] -> Type -> Type -> Coercion
mkPluginUnivCo CommandLineOption
"ghc-typelits-extra" Role
Nominal []
             (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
args) Type
res


decideEqualSOP :: ExtraDefs -> [Ct] -> [Ct] -> TcPluginM 'Solve TcPluginSolveResult
decideEqualSOP :: ExtraDefs -> TcPluginSolver
decideEqualSOP ExtraDefs
_    [Ct]
_givens []      = TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
TcPluginOk [] [])
decideEqualSOP ExtraDefs
defs [Ct]
givens  [Ct]
wanteds = do
  let givensTyConSubst :: TyConSubst
givensTyConSubst = [Ct] -> TyConSubst
mkTyConSubst [Ct]
givens
  [SolverConstraint]
unit_wanteds <- [Maybe SolverConstraint] -> [SolverConstraint]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe SolverConstraint] -> [SolverConstraint])
-> TcPluginM 'Solve [Maybe SolverConstraint]
-> TcPluginM 'Solve [SolverConstraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ct -> TcPluginM 'Solve (Maybe SolverConstraint))
-> [Ct] -> TcPluginM 'Solve [Maybe SolverConstraint]
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 (MaybeT (TcPluginM 'Solve) SolverConstraint
-> TcPluginM 'Solve (Maybe SolverConstraint)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TcPluginM 'Solve) SolverConstraint
 -> TcPluginM 'Solve (Maybe SolverConstraint))
-> (Ct -> MaybeT (TcPluginM 'Solve) SolverConstraint)
-> Ct
-> TcPluginM 'Solve (Maybe SolverConstraint)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtraDefs
-> TyConSubst -> Ct -> MaybeT (TcPluginM 'Solve) SolverConstraint
toSolverConstraint ExtraDefs
defs TyConSubst
givensTyConSubst) [Ct]
wanteds
  case [SolverConstraint]
unit_wanteds of
    [] -> TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
TcPluginOk [] [])
    [SolverConstraint]
_  -> do
      [SolverConstraint]
unit_givens <- [Maybe SolverConstraint] -> [SolverConstraint]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe SolverConstraint] -> [SolverConstraint])
-> TcPluginM 'Solve [Maybe SolverConstraint]
-> TcPluginM 'Solve [SolverConstraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ct -> TcPluginM 'Solve (Maybe SolverConstraint))
-> [Ct] -> TcPluginM 'Solve [Maybe SolverConstraint]
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 (MaybeT (TcPluginM 'Solve) SolverConstraint
-> TcPluginM 'Solve (Maybe SolverConstraint)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TcPluginM 'Solve) SolverConstraint
 -> TcPluginM 'Solve (Maybe SolverConstraint))
-> (Ct -> MaybeT (TcPluginM 'Solve) SolverConstraint)
-> Ct
-> TcPluginM 'Solve (Maybe SolverConstraint)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtraDefs
-> TyConSubst -> Ct -> MaybeT (TcPluginM 'Solve) SolverConstraint
toSolverConstraint ExtraDefs
defs TyConSubst
givensTyConSubst) [Ct]
givens
      SimplifyResult
sr <- ExtraDefs -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
simplifyExtra ExtraDefs
defs ([SolverConstraint]
unit_givens [SolverConstraint] -> [SolverConstraint] -> [SolverConstraint]
forall a. [a] -> [a] -> [a]
++ [SolverConstraint]
unit_wanteds)
      CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"ghc-typelits-extra Wanteds {" (SDoc -> TcPluginM 'Solve ()) -> SDoc -> TcPluginM 'Solve ()
forall a b. (a -> b) -> a -> b
$
        [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"givens:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
givens
             , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"unit_givens" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SolverConstraint] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [SolverConstraint]
unit_givens
             , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text (CommandLineOption -> SDoc) -> CommandLineOption -> SDoc
forall a b. (a -> b) -> a -> b
$ Int -> Char -> CommandLineOption
forall a. Int -> a -> [a]
replicate Int
80 Char
'-'
             , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"wanteds:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
wanteds
             , CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"unit_wanteds:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SolverConstraint] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [SolverConstraint]
unit_wanteds
             ]
      CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"normalised" (SimplifyResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr SimplifyResult
sr)
      case SimplifyResult
sr of
        Simplified [(EvTerm, Ct)]
evs [Ct]
new -> TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
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) [Ct]
new)
        Impossible SolverConstraint
eq  -> TcPluginSolveResult -> TcPluginM 'Solve TcPluginSolveResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Ct] -> TcPluginSolveResult
TcPluginContradiction [SolverConstraint -> Ct
fromSolverConstraint SolverConstraint
eq])

data SolverConstraint
   = NatEquality Ct ExtraOp ExtraOp Normalised
   | NatInequality Ct [Coercion] ExtraOp ExtraOp Bool Normalised

instance Outputable SolverConstraint where
  ppr :: SolverConstraint -> SDoc
ppr (NatEquality Ct
ct ExtraOp
op1 ExtraOp
op2 Normalised
norm) =
    CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"NatEquality" SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
op1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
op2 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Normalised -> SDoc
forall a. Outputable a => a -> SDoc
ppr Normalised
norm
  ppr (NatInequality Ct
_ [Coercion]
_ ExtraOp
op1 ExtraOp
op2 Bool
b Normalised
norm) =
    CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"NatInequality" SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
op1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
op2 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
b SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Normalised -> SDoc
forall a. Outputable a => a -> SDoc
ppr Normalised
norm

data SimplifyResult
  = Simplified [(EvTerm,Ct)] [Ct]
  | Impossible SolverConstraint

instance Outputable SimplifyResult where
  ppr :: SimplifyResult -> SDoc
ppr (Simplified [(EvTerm, Ct)]
evs [Ct]
new) =
    CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"Simplified" SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"Solved:" SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [(EvTerm, Ct)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(EvTerm, Ct)]
evs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"New:" SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
new
  ppr (Impossible SolverConstraint
sct) =
    CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text CommandLineOption
"Impossible" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SolverConstraint -> SDoc
forall a. Outputable a => a -> SDoc
ppr SolverConstraint
sct

simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
simplifyExtra ExtraDefs
defs [SolverConstraint]
eqs = CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"simplifyExtra" ([SolverConstraint] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [SolverConstraint]
eqs) TcPluginM 'Solve ()
-> TcPluginM 'Solve SimplifyResult
-> TcPluginM 'Solve SimplifyResult
forall a b.
TcPluginM 'Solve a -> TcPluginM 'Solve b -> TcPluginM 'Solve b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Maybe (EvTerm, Ct)]
-> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
simples [] [] [SolverConstraint]
eqs
  where
    simples :: [Maybe (EvTerm, Ct)] -> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
    simples :: [Maybe (EvTerm, Ct)]
-> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
simples [Maybe (EvTerm, Ct)]
evs [Ct]
news [] = SimplifyResult -> TcPluginM 'Solve SimplifyResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(EvTerm, Ct)] -> [Ct] -> SimplifyResult
Simplified ([Maybe (EvTerm, Ct)] -> [(EvTerm, Ct)]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (EvTerm, Ct)]
evs) [Ct]
news)
    simples [Maybe (EvTerm, Ct)]
evs [Ct]
news (eq :: SolverConstraint
eq@(NatEquality Ct
ct ExtraOp
u ExtraOp
v Normalised
norm):[SolverConstraint]
eqs') = do
      UnifyResult
ur <- Ct -> ExtraOp -> ExtraOp -> TcPluginM 'Solve UnifyResult
unifyExtra Ct
ct ExtraOp
u ExtraOp
v
      CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"unifyExtra result" (UnifyResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr UnifyResult
ur)
      let evM :: Maybe EvTerm
evM = LookedUpTyCons -> Ct -> [Coercion] -> Maybe EvTerm
evMagic (ExtraDefs -> LookedUpTyCons
ordTyCons ExtraDefs
defs) Ct
ct (Normalised -> [Coercion]
depsFromNormalised Normalised
norm)
      case UnifyResult
ur of
        UnifyResult
Win -> [Maybe (EvTerm, Ct)]
-> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
simples ((EvTerm -> (EvTerm, Ct)) -> Maybe EvTerm -> Maybe (EvTerm, Ct)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,Ct
ct) Maybe EvTerm
evMMaybe (EvTerm, Ct) -> [Maybe (EvTerm, Ct)] -> [Maybe (EvTerm, Ct)]
forall a. a -> [a] -> [a]
:[Maybe (EvTerm, Ct)]
evs) [Ct]
news [SolverConstraint]
eqs'
        UnifyResult
Lose | [Maybe (EvTerm, Ct)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Maybe (EvTerm, Ct)]
evs Bool -> Bool -> Bool
&& [SolverConstraint] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SolverConstraint]
eqs' -> SimplifyResult -> TcPluginM 'Solve SimplifyResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (SolverConstraint -> SimplifyResult
Impossible SolverConstraint
eq)
        UnifyResult
_ | Normalised {} <- Normalised
norm
          , Ct -> Bool
isWantedCt Ct
ct -> do
          Ct
newCt <- ExtraDefs -> SolverConstraint -> TcPluginM 'Solve Ct
createWantedFromNormalised ExtraDefs
defs SolverConstraint
eq
          [Maybe (EvTerm, Ct)]
-> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
simples ((EvTerm -> (EvTerm, Ct)) -> Maybe EvTerm -> Maybe (EvTerm, Ct)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,Ct
ct) Maybe EvTerm
evMMaybe (EvTerm, Ct) -> [Maybe (EvTerm, Ct)] -> [Maybe (EvTerm, Ct)]
forall a. a -> [a] -> [a]
:[Maybe (EvTerm, Ct)]
evs) (Ct
newCtCt -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
:[Ct]
news) [SolverConstraint]
eqs'
        UnifyResult
Lose -> [Maybe (EvTerm, Ct)]
-> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
simples [Maybe (EvTerm, Ct)]
evs [Ct]
news [SolverConstraint]
eqs'
        UnifyResult
Draw -> [Maybe (EvTerm, Ct)]
-> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
simples [Maybe (EvTerm, Ct)]
evs [Ct]
news [SolverConstraint]
eqs'
    simples [Maybe (EvTerm, Ct)]
evs [Ct]
news (eq :: SolverConstraint
eq@(NatInequality Ct
ct [Coercion]
deps ExtraOp
u ExtraOp
v Bool
b Normalised
norm):[SolverConstraint]
eqs') = do
      CommandLineOption -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *).
MonadTcPlugin m =>
CommandLineOption -> SDoc -> m ()
tcPluginTrace CommandLineOption
"unifyExtra leq result" ((ExtraOp, ExtraOp, Bool) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (ExtraOp
u,ExtraOp
v,Bool
b))
      let evM :: Maybe EvTerm
evM = LookedUpTyCons -> Ct -> [Coercion] -> Maybe EvTerm
evMagic (ExtraDefs -> LookedUpTyCons
ordTyCons ExtraDefs
defs) Ct
ct ([Coercion]
deps [Coercion] -> [Coercion] -> [Coercion]
forall a. Semigroup a => a -> a -> a
<> Normalised -> [Coercion]
depsFromNormalised Normalised
norm)
      case (ExtraOp
u,ExtraOp
v) of
        (I Integer
i,I 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)]
-> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
simples ((EvTerm -> (EvTerm, Ct)) -> Maybe EvTerm -> Maybe (EvTerm, Ct)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,Ct
ct) Maybe EvTerm
evMMaybe (EvTerm, Ct) -> [Maybe (EvTerm, Ct)] -> [Maybe (EvTerm, Ct)]
forall a. a -> [a] -> [a]
:[Maybe (EvTerm, Ct)]
evs) [Ct]
news [SolverConstraint]
eqs'
          | Bool
otherwise     -> SimplifyResult -> TcPluginM 'Solve SimplifyResult
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return  (SolverConstraint -> SimplifyResult
Impossible SolverConstraint
eq)
        (ExtraOp
p, Max ExtraOp
x 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)]
-> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
simples ((EvTerm -> (EvTerm, Ct)) -> Maybe EvTerm -> Maybe (EvTerm, Ct)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,Ct
ct) Maybe EvTerm
evMMaybe (EvTerm, Ct) -> [Maybe (EvTerm, Ct)] -> [Maybe (EvTerm, Ct)]
forall a. a -> [a] -> [a]
:[Maybe (EvTerm, Ct)]
evs) [Ct]
news [SolverConstraint]
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'
        (ExtraOp
p, q :: ExtraOp
q@(V TyVar
_))
          | Bool
b -> case ExtraOp -> [SolverConstraint] -> Maybe (Coercion, ExtraOp)
findMax ExtraOp
q [SolverConstraint]
eqs of
                   Just (Coercion
i,ExtraOp
m) ->
                      [Maybe (EvTerm, Ct)]
-> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
simples [Maybe (EvTerm, Ct)]
evs [Ct]
news
                        (Ct
-> [Coercion]
-> ExtraOp
-> ExtraOp
-> Bool
-> Normalised
-> SolverConstraint
NatInequality Ct
ct (Coercion
iCoercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
:[Coercion]
deps) ExtraOp
p ExtraOp
m Bool
b Normalised
normSolverConstraint -> [SolverConstraint] -> [SolverConstraint]
forall a. a -> [a] -> [a]
:[SolverConstraint]
eqs')
                   Maybe (Coercion, ExtraOp)
Nothing -> [Maybe (EvTerm, Ct)]
-> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
simples [Maybe (EvTerm, Ct)]
evs [Ct]
news [SolverConstraint]
eqs'
        (ExtraOp, ExtraOp)
_ | Normalised {} <- Normalised
norm
          , Ct -> Bool
isWantedCt Ct
ct -> do
          Ct
newCt <- ExtraDefs -> SolverConstraint -> TcPluginM 'Solve Ct
createWantedFromNormalised ExtraDefs
defs SolverConstraint
eq
          [Maybe (EvTerm, Ct)]
-> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
simples ((EvTerm -> (EvTerm, Ct)) -> Maybe EvTerm -> Maybe (EvTerm, Ct)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,Ct
ct) Maybe EvTerm
evMMaybe (EvTerm, Ct) -> [Maybe (EvTerm, Ct)] -> [Maybe (EvTerm, Ct)]
forall a. a -> [a] -> [a]
:[Maybe (EvTerm, Ct)]
evs) (Ct
newCtCt -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
:[Ct]
news) [SolverConstraint]
eqs'
        (ExtraOp, ExtraOp)
_ -> [Maybe (EvTerm, Ct)]
-> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult
simples [Maybe (EvTerm, Ct)]
evs [Ct]
news [SolverConstraint]
eqs'

    -- look for given constraint with the form: c ~ Max x y
    findMax :: ExtraOp -> [SolverConstraint] -> Maybe (Coercion, ExtraOp)
    findMax :: ExtraOp -> [SolverConstraint] -> Maybe (Coercion, ExtraOp)
findMax ExtraOp
c = [SolverConstraint] -> Maybe (Coercion, ExtraOp)
go
      where
        go :: [SolverConstraint] -> Maybe (Coercion, ExtraOp)
go [] = Maybe (Coercion, ExtraOp)
forall a. Maybe a
Nothing
        go ((NatEquality Ct
ct ExtraOp
a b :: ExtraOp
b@(Max ExtraOp
_ ExtraOp
_) Normalised
_) :[SolverConstraint]
_)
          | 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)
            = (Coercion, ExtraOp) -> Maybe (Coercion, ExtraOp)
forall a. a -> Maybe a
Just (HasDebugCallStack => CtEvidence -> Coercion
CtEvidence -> Coercion
ctEvCoercion (Ct -> CtEvidence
ctEvidence Ct
ct), ExtraOp
b)
        go ((NatEquality Ct
ct a :: ExtraOp
a@(Max ExtraOp
_ ExtraOp
_) ExtraOp
b Normalised
_) :[SolverConstraint]
_)
          | 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)
            = (Coercion, ExtraOp) -> Maybe (Coercion, ExtraOp)
forall a. a -> Maybe a
Just (HasDebugCallStack => CtEvidence -> Coercion
CtEvidence -> Coercion
ctEvCoercion (Ct -> CtEvidence
ctEvidence Ct
ct), ExtraOp
a)
        go (SolverConstraint
_:[SolverConstraint]
rest) = [SolverConstraint] -> Maybe (Coercion, ExtraOp)
go [SolverConstraint]
rest


-- Extract the Nat equality constraints
toSolverConstraint :: ExtraDefs -> TyConSubst -> Ct -> MaybeT (TcPluginM 'Solve) SolverConstraint
toSolverConstraint :: ExtraDefs
-> TyConSubst -> Ct -> MaybeT (TcPluginM 'Solve) SolverConstraint
toSolverConstraint ExtraDefs
defs TyConSubst
givensTyConSubst Ct
ct =
    case LookedUpTyCons
-> TyConSubst -> Type -> Maybe (Relation, [Coercion])
isNatRel (ExtraDefs -> LookedUpTyCons
ordTyCons ExtraDefs
defs) TyConSubst
givensTyConSubst Type
ty0 of
      Maybe (Relation, [Coercion])
Nothing -> CommandLineOption -> MaybeT (TcPluginM 'Solve) SolverConstraint
forall a. CommandLineOption -> MaybeT (TcPluginM 'Solve) a
forall (m :: * -> *) a. MonadFail m => CommandLineOption -> m a
fail CommandLineOption
"Nothing"
      Just (((Type
t1,Type
t2),Maybe Bool
leqM),[Coercion]
deps) -> do
        (ExtraOp
t1', Normalised
n1) <- ExtraDefs
-> Type -> MaybeT (TcPluginM 'Solve) (ExtraOp, Normalised)
normaliseNat ExtraDefs
defs Type
t1
        (ExtraOp
t2', Normalised
n2) <- ExtraDefs
-> Type -> MaybeT (TcPluginM 'Solve) (ExtraOp, Normalised)
normaliseNat ExtraDefs
defs Type
t2
        case Maybe Bool
leqM of
          Maybe Bool
Nothing ->
            SolverConstraint -> MaybeT (TcPluginM 'Solve) SolverConstraint
forall a. a -> MaybeT (TcPluginM 'Solve) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ct -> ExtraOp -> ExtraOp -> Normalised -> SolverConstraint
NatEquality Ct
ct ExtraOp
t1' ExtraOp
t2' (Normalised -> Normalised -> Normalised
mergeNormalised Normalised
n1 Normalised
n2))
          Just Bool
b ->
            SolverConstraint -> MaybeT (TcPluginM 'Solve) SolverConstraint
forall a. a -> MaybeT (TcPluginM 'Solve) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ct
-> [Coercion]
-> ExtraOp
-> ExtraOp
-> Bool
-> Normalised
-> SolverConstraint
NatInequality Ct
ct [Coercion]
deps ExtraOp
t1' ExtraOp
t2' Bool
b (Normalised -> Normalised -> Normalised
mergeNormalised Normalised
n1 Normalised
n2))
  where
   ty0 :: Type
ty0 = CtEvidence -> Type
ctEvPred (Ct -> CtEvidence
ctEvidence Ct
ct)

createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM 'Solve Ct
createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM 'Solve Ct
createWantedFromNormalised ExtraDefs
defs SolverConstraint
sct = do
  let extractCtSides :: SolverConstraint -> (Ct, Type, Type)
extractCtSides (NatEquality Ct
ct ExtraOp
t1 ExtraOp
t2 Normalised
_)   = (Ct
ct, ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
t1, ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
t2)
      extractCtSides (NatInequality Ct
ct [Coercion]
_ ExtraOp
x ExtraOp
y Bool
b Normalised
_) =
        let t1 :: Type
t1 = LookedUpTyCons -> Type -> Type -> Type
mkLeqQNat (ExtraDefs -> LookedUpTyCons
ordTyCons ExtraDefs
defs) (ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
x) (ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
y)
            tb :: TyCon
tb = if Bool
b then TyCon
promotedTrueDataCon else TyCon
promotedFalseDataCon
            t2 :: Type
t2 = TyCon -> [Type] -> Type
TyConApp TyCon
tb []
          in (Ct
ct, Type
t1, Type
t2)
  let (Ct
ct, Type
t1, Type
t2) = SolverConstraint -> (Ct, Type, Type)
extractCtSides SolverConstraint
sct
  Type
newPredTy <- LookedUpTyCons -> Ct -> Type -> Type -> TcPluginM 'Solve Type
forall (m :: * -> *).
Monad m =>
LookedUpTyCons -> Ct -> Type -> Type -> m Type
toLeqPredType (ExtraDefs -> LookedUpTyCons
ordTyCons ExtraDefs
defs) Ct
ct Type
t1 Type
t2
  CtEvidence
ev <- CtLoc -> Type -> TcPluginM 'Solve CtEvidence
forall (m :: * -> *).
MonadTcPluginWork m =>
CtLoc -> Type -> m CtEvidence
newWanted (Ct -> CtLoc
ctLoc Ct
ct) Type
newPredTy
  Ct -> TcPluginM 'Solve Ct
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ct -> CtEvidence -> Ct
setCtEv Ct
ct CtEvidence
ev)

fromSolverConstraint :: SolverConstraint -> Ct
fromSolverConstraint :: SolverConstraint -> Ct
fromSolverConstraint (NatEquality Ct
ct ExtraOp
_ ExtraOp
_ Normalised
_)  = Ct
ct
fromSolverConstraint (NatInequality Ct
ct [Coercion]
_ ExtraOp
_ ExtraOp
_ Bool
_ Normalised
_) = Ct
ct

-- Utils
evMagic :: LookedUpTyCons -> Ct -> [Coercion] -> Maybe EvTerm
evMagic :: LookedUpTyCons -> Ct -> [Coercion] -> Maybe EvTerm
evMagic LookedUpTyCons
tcs Ct
ct [Coercion]
deps = case Type -> Pred
classifyPredType (Type -> Pred) -> Type -> Pred
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
    EqPred EqRel
NomEq Type
t1 Type
t2 ->
      let ctEv :: Coercion
ctEv = CommandLineOption -> Role -> [Coercion] -> Type -> Type -> Coercion
mkPluginUnivCo CommandLineOption
"ghc-typelits-extra" Role
Nominal [Coercion]
deps Type
t1 Type
t2
       in EvTerm -> Maybe EvTerm
forall a. a -> Maybe a
Just (EvExpr -> EvTerm
EvExpr (Coercion -> EvExpr
forall b. Coercion -> Expr b
Coercion Coercion
ctEv))
    IrredPred Type
p ->
      let t1 :: Type
t1 = TyCon -> [Type] -> Type
mkTyConApp (LookedUpTyCons -> TyCon
c0TyCon LookedUpTyCons
tcs) []
          co :: Coercion
co = CommandLineOption -> Role -> [Coercion] -> Type -> Type -> Coercion
mkPluginUnivCo CommandLineOption
"ghc-typelits-extra" Role
Representational [Coercion]
deps Type
t1 Type
p
          dcApp :: EvExpr
dcApp = TyVar -> EvExpr
evId (DataCon -> TyVar
dataConWrapId (LookedUpTyCons -> DataCon
c0DataCon LookedUpTyCons
tcs))
       in EvTerm -> Maybe EvTerm
forall a. a -> Maybe a
Just (EvExpr -> EvTerm
EvExpr (EvExpr -> Coercion -> EvExpr
evCast EvExpr
dcApp Coercion
co))
    Pred
_ -> Maybe EvTerm
forall a. Maybe a
Nothing