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

{-# LANGUAGE CPP                        #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MagicHash                  #-}
{-# LANGUAGE RecordWildCards            #-}

{-# OPTIONS_GHC -fno-warn-unused-imports #-}
#if __GLASGOW_HASKELL__ < 801
#define nonDetCmpType cmpType
#endif

module GHC.TypeLits.Normalise.Unify
  ( -- * 'Nat' expressions \<-\> 'SOP' terms
    CType (..)
  , CoreSOP
  , normaliseNat
  , normaliseNatEverywhere
  , normaliseSimplifyNat
  , reifySOP
    -- * Substitution on 'SOP' terms
  , UnifyItem (..)
  , CoreUnify
  , substsSOP
  , substsSubst
    -- * Find unifiers
  , UnifyResult (..)
  , unifyNats
  , unifiers
    -- * Free variables in 'SOP' terms
  , fvSOP
    -- * Inequalities
  , subtractIneq
  , solveIneq
  , ineqToSubst
  , subtractionToPred
  , instantSolveIneq
  , solvedInEqSmallestConstraint
    -- * Properties
  , isNatural
  )
where

-- External
import Control.Arrow (first, second)
import Control.Monad.Trans.Writer.Strict
import Data.Function (on)
import Data.List     ((\\), intersect, nub)
import Data.Maybe    (fromMaybe, mapMaybe, isJust)
import Data.Set      (Set)
import qualified Data.Set as Set

import GHC.Base               (isTrue#,(==#))
import GHC.Integer            (smallInteger)
import GHC.Integer.Logarithms (integerLogBase#)

-- GHC API
#if MIN_VERSION_ghc(9,0,0)
import GHC.Builtin.Types (boolTy, promotedTrueDataCon, typeNatKind)
import GHC.Builtin.Types.Literals
  (typeNatAddTyCon, typeNatExpTyCon, typeNatLeqTyCon, typeNatMulTyCon, typeNatSubTyCon)
import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType, mkPrimEqPred)
import GHC.Core.TyCon (TyCon)
import GHC.Core.Type
  (PredType, TyVar, coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy, nonDetCmpType, typeKind)
import GHC.Core.TyCo.Rep (Kind, Type (..), TyLit (..))
import GHC.Tc.Plugin (TcPluginM, tcPluginTrace)
import GHC.Tc.Types.Constraint (Ct, ctEvidence, ctEvId, ctEvPred, isGiven)
import GHC.Types.Unique.Set
  (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets, unitUniqSet)
import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)
#else
import Outputable    (Outputable (..), (<+>), ($$), text)
import TcPluginM     (TcPluginM, tcPluginTrace)
import TcTypeNats    (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,
                      typeNatSubTyCon, typeNatLeqTyCon)
import TyCon         (TyCon)
import Type          (TyVar,
                      coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy,
                      nonDetCmpType, PredType, typeKind)
import TyCoRep       (Kind, Type (..), TyLit (..))
import TysWiredIn    (boolTy, promotedTrueDataCon, typeNatKind)
import UniqSet       (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets,
                      unitUniqSet)

#if MIN_VERSION_ghc(8,10,0)
import Constraint (Ct,  ctEvidence, ctEvId, ctEvPred, isGiven)
import Predicate  (EqRel (NomEq), Pred (EqPred), classifyPredType, mkPrimEqPred)
#else
import TcRnMonad  (Ct, ctEvidence, isGiven)
import TcRnTypes  (ctEvPred)
import Type       (EqRel (NomEq), PredTree (EqPred), classifyPredType, mkPrimEqPred)
#endif
#endif

-- Internal
import GHC.TypeLits.Normalise.SOP

-- Used for haddock
import GHC.TypeLits (Nat)

newtype CType = CType { CType -> Type
unCType :: Type }
  deriving Rational -> CType -> SDoc
CType -> SDoc
(CType -> SDoc) -> (Rational -> CType -> SDoc) -> Outputable CType
forall a. (a -> SDoc) -> (Rational -> a -> SDoc) -> Outputable a
pprPrec :: Rational -> CType -> SDoc
$cpprPrec :: Rational -> CType -> SDoc
ppr :: CType -> SDoc
$cppr :: CType -> SDoc
Outputable

instance Eq CType where
  (CType Type
ty1) == :: CType -> CType -> Bool
== (CType Type
ty2) = Type -> Type -> Bool
eqType Type
ty1 Type
ty2

instance Ord CType where
  compare :: CType -> CType -> Ordering
compare (CType Type
ty1) (CType Type
ty2) = Type -> Type -> Ordering
nonDetCmpType Type
ty1 Type
ty2

-- | 'SOP' with 'TyVar' variables
type CoreSOP     = SOP TyVar CType
type CoreProduct = Product TyVar CType
type CoreSymbol  = Symbol TyVar CType

-- | Convert a type of /kind/ 'GHC.TypeLits.Nat' to an 'SOP' term, but
-- only when the type is constructed out of:
--
-- * literals
-- * type variables
-- * Applications of the arithmetic operators @(+,-,*,^)@
normaliseNat :: Type -> Writer [(Type,Type)] CoreSOP
normaliseNat :: Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
ty | Just Type
ty1 <- Type -> Maybe Type
coreView Type
ty = Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
ty1
normaliseNat (TyVarTy Var
v)          = CoreSOP -> Writer [(Type, Type)] CoreSOP
forall (m :: * -> *) a. Monad m => a -> m a
return ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Var -> Symbol Var CType
forall v c. v -> Symbol v c
V Var
v]])
normaliseNat (LitTy (NumTyLit Integer
i)) = CoreSOP -> Writer [(Type, Type)] CoreSOP
forall (m :: * -> *) a. Monad m => a -> m a
return ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
i]])
normaliseNat (TyConApp TyCon
tc [Type
x,Type
y])
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatAddTyCon = CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd (CoreSOP -> CoreSOP -> CoreSOP)
-> Writer [(Type, Type)] CoreSOP
-> WriterT [(Type, Type)] Identity (CoreSOP -> CoreSOP)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x WriterT [(Type, Type)] Identity (CoreSOP -> CoreSOP)
-> Writer [(Type, Type)] CoreSOP -> Writer [(Type, Type)] CoreSOP
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatSubTyCon = do
    [(Type, Type)] -> WriterT [(Type, Type)] Identity ()
forall (m :: * -> *) w. Monad m => w -> WriterT w m ()
tell [(Type
x,Type
y)]
    CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd (CoreSOP -> CoreSOP -> CoreSOP)
-> Writer [(Type, Type)] CoreSOP
-> WriterT [(Type, Type)] Identity (CoreSOP -> CoreSOP)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x
                WriterT [(Type, Type)] Identity (CoreSOP -> CoreSOP)
-> Writer [(Type, Type)] CoreSOP -> Writer [(Type, Type)] CoreSOP
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I (-Integer
1)]]) (CoreSOP -> CoreSOP)
-> Writer [(Type, Type)] CoreSOP -> Writer [(Type, Type)] CoreSOP
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y)
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatMulTyCon = CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul (CoreSOP -> CoreSOP -> CoreSOP)
-> Writer [(Type, Type)] CoreSOP
-> WriterT [(Type, Type)] Identity (CoreSOP -> CoreSOP)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x WriterT [(Type, Type)] Identity (CoreSOP -> CoreSOP)
-> Writer [(Type, Type)] CoreSOP -> Writer [(Type, Type)] CoreSOP
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatExpTyCon = CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
normaliseExp (CoreSOP -> CoreSOP -> CoreSOP)
-> Writer [(Type, Type)] CoreSOP
-> WriterT [(Type, Type)] Identity (CoreSOP -> CoreSOP)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
x WriterT [(Type, Type)] Identity (CoreSOP -> CoreSOP)
-> Writer [(Type, Type)] CoreSOP -> Writer [(Type, Type)] CoreSOP
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
y
normaliseNat Type
t = CoreSOP -> Writer [(Type, Type)] CoreSOP
forall (m :: * -> *) a. Monad m => a -> m a
return ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [CType -> Symbol Var CType
forall v c. c -> Symbol v c
C (Type -> CType
CType Type
t)]])

-- | Runs writer action. If the result /Nothing/ writer actions will be
-- discarded.
maybeRunWriter
  :: Monoid a
  => Writer a (Maybe b)
  -> Writer a (Maybe b)
maybeRunWriter :: Writer a (Maybe b) -> Writer a (Maybe b)
maybeRunWriter Writer a (Maybe b)
w =
  case Writer a (Maybe b) -> (Maybe b, a)
forall w a. Writer w a -> (a, w)
runWriter Writer a (Maybe b)
w of
    (Maybe b
Nothing, a
_) -> Maybe b -> Writer a (Maybe b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe b
forall a. Maybe a
Nothing
    (Maybe b
b, a
a) -> a -> WriterT a Identity ()
forall (m :: * -> *) w. Monad m => w -> WriterT w m ()
tell a
a WriterT a Identity () -> Writer a (Maybe b) -> Writer a (Maybe b)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe b -> Writer a (Maybe b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe b
b

-- | Applies 'normaliseNat' and 'simplifySOP' to type or predicates to reduce
-- any occurrences of sub-terms of /kind/ 'GHC.TypeLits.Nat'. If the result is
-- the same as input, returns @'Nothing'@.
normaliseNatEverywhere :: Type -> Writer [(Type, Type)] (Maybe Type)
normaliseNatEverywhere :: Type -> Writer [(Type, Type)] (Maybe Type)
normaliseNatEverywhere Type
ty0
  | TyConApp TyCon
tc [Type]
_fields <- Type
ty0
  , TyCon
tc TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TyCon]
knownTyCons = do
    -- Normalize under current type constructor application. 'go' skips all
    -- known type constructors.
    Maybe Type
ty1M <- Writer [(Type, Type)] (Maybe Type)
-> Writer [(Type, Type)] (Maybe Type)
forall a b. Monoid a => Writer a (Maybe b) -> Writer a (Maybe b)
maybeRunWriter (Type -> Writer [(Type, Type)] (Maybe Type)
go Type
ty0)
    let ty1 :: Type
ty1 = Type -> Maybe Type -> Type
forall a. a -> Maybe a -> a
fromMaybe Type
ty0 Maybe Type
ty1M

    -- Normalize (subterm-normalized) type given to 'normaliseNatEverywhere'
    Type
ty2 <- Type -> Writer [(Type, Type)] Type
normaliseSimplifyNat Type
ty1
    -- TODO: 'normaliseNat' could keep track whether it changed anything. That's
    -- TODO: probably cheaper than checking for equality here.
    Maybe Type -> Writer [(Type, Type)] (Maybe Type)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (if Type
ty2 Type -> Type -> Bool
`eqType` Type
ty1 then Maybe Type
ty1M else Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty2)
  | Bool
otherwise = Type -> Writer [(Type, Type)] (Maybe Type)
go Type
ty0
 where
  knownTyCons :: [TyCon]
  knownTyCons :: [TyCon]
knownTyCons = [TyCon
typeNatExpTyCon, TyCon
typeNatMulTyCon, TyCon
typeNatSubTyCon, TyCon
typeNatAddTyCon]

  -- Normalize given type, but ignore all top-level
  go :: Type -> Writer [(Type, Type)] (Maybe Type)
  go :: Type -> Writer [(Type, Type)] (Maybe Type)
go (TyConApp TyCon
tc_ [Type]
fields0_) = do
    [Maybe Type]
fields1_ <- (Type -> Writer [(Type, Type)] (Maybe Type))
-> [Type] -> WriterT [(Type, Type)] Identity [Maybe Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Writer [(Type, Type)] (Maybe Type)
-> Writer [(Type, Type)] (Maybe Type)
forall a b. Monoid a => Writer a (Maybe b) -> Writer a (Maybe b)
maybeRunWriter (Writer [(Type, Type)] (Maybe Type)
 -> Writer [(Type, Type)] (Maybe Type))
-> (Type -> Writer [(Type, Type)] (Maybe Type))
-> Type
-> Writer [(Type, Type)] (Maybe Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Writer [(Type, Type)] (Maybe Type)
cont) [Type]
fields0_
    if (Maybe Type -> Bool) -> [Maybe Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust [Maybe Type]
fields1_ then
      Maybe Type -> Writer [(Type, Type)] (Maybe Type)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Maybe Type
forall a. a -> Maybe a
Just (TyCon -> [Type] -> Type
TyConApp TyCon
tc_ ((Type -> Maybe Type -> Type) -> [Type] -> [Maybe Type] -> [Type]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type -> Maybe Type -> Type
forall a. a -> Maybe a -> a
fromMaybe [Type]
fields0_ [Maybe Type]
fields1_)))
    else
      Maybe Type -> Writer [(Type, Type)] (Maybe Type)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Type
forall a. Maybe a
Nothing
   where
    cont :: Type -> Writer [(Type, Type)] (Maybe Type)
cont = if TyCon
tc_ TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TyCon]
knownTyCons then Type -> Writer [(Type, Type)] (Maybe Type)
go else Type -> Writer [(Type, Type)] (Maybe Type)
normaliseNatEverywhere
  go Type
_ = Maybe Type -> Writer [(Type, Type)] (Maybe Type)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Type
forall a. Maybe a
Nothing

normaliseSimplifyNat :: Type -> Writer [(Type, Type)] Type
normaliseSimplifyNat :: Type -> Writer [(Type, Type)] Type
normaliseSimplifyNat Type
ty
  | HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty Type -> Type -> Bool
`eqType` Type
typeNatKind = do
      CoreSOP
ty' <- Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
ty
      Type -> Writer [(Type, Type)] Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Writer [(Type, Type)] Type)
-> Type -> Writer [(Type, Type)] Type
forall a b. (a -> b) -> a -> b
$ CoreSOP -> Type
reifySOP (CoreSOP -> Type) -> CoreSOP -> Type
forall a b. (a -> b) -> a -> b
$ CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c
simplifySOP CoreSOP
ty'
  | Bool
otherwise = Type -> Writer [(Type, Type)] Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty

-- | Convert a 'SOP' term back to a type of /kind/ 'GHC.TypeLits.Nat'
reifySOP :: CoreSOP -> Type
reifySOP :: CoreSOP -> Type
reifySOP = [Either (Product Var CType) (Product Var CType)] -> Type
combineP ([Either (Product Var CType) (Product Var CType)] -> Type)
-> (CoreSOP -> [Either (Product Var CType) (Product Var CType)])
-> CoreSOP
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Product Var CType
 -> Either (Product Var CType) (Product Var CType))
-> [Product Var CType]
-> [Either (Product Var CType) (Product Var CType)]
forall a b. (a -> b) -> [a] -> [b]
map Product Var CType -> Either (Product Var CType) (Product Var CType)
negateP ([Product Var CType]
 -> [Either (Product Var CType) (Product Var CType)])
-> (CoreSOP -> [Product Var CType])
-> CoreSOP
-> [Either (Product Var CType) (Product Var CType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreSOP -> [Product Var CType]
forall v c. SOP v c -> [Product v c]
unS
  where
    negateP :: CoreProduct -> Either CoreProduct CoreProduct
    negateP :: Product Var CType -> Either (Product Var CType) (Product Var CType)
negateP (P ((I Integer
i):ps :: [Symbol Var CType]
ps@(Symbol Var CType
_:[Symbol Var CType]
_))) | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== (-Integer
1) = Product Var CType -> Either (Product Var CType) (Product Var CType)
forall a b. a -> Either a b
Left  ([Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
ps)
    negateP (P ((I Integer
i):[Symbol Var CType]
ps)) | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0           = Product Var CType -> Either (Product Var CType) (Product Var CType)
forall a b. a -> Either a b
Left  ([Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P ((Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I (Integer -> Integer
forall a. Num a => a -> a
abs Integer
i))Symbol Var CType -> [Symbol Var CType] -> [Symbol Var CType]
forall a. a -> [a] -> [a]
:[Symbol Var CType]
ps))
    negateP Product Var CType
ps                               = Product Var CType -> Either (Product Var CType) (Product Var CType)
forall a b. b -> Either a b
Right Product Var CType
ps

    combineP :: [Either CoreProduct CoreProduct] -> Type
    combineP :: [Either (Product Var CType) (Product Var CType)] -> Type
combineP []     = Integer -> Type
mkNumLitTy Integer
0
    combineP [Either (Product Var CType) (Product Var CType)
p]    = (Product Var CType -> Type)
-> (Product Var CType -> Type)
-> Either (Product Var CType) (Product Var CType)
-> Type
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\Product Var CType
p' -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon
                                                [Integer -> Type
mkNumLitTy Integer
0, Product Var CType -> Type
reifyProduct Product Var CType
p'])
                             Product Var CType -> Type
reifyProduct Either (Product Var CType) (Product Var CType)
p
    combineP [Either (Product Var CType) (Product Var CType)
p1,Either (Product Var CType) (Product Var CType)
p2] = (Product Var CType -> Type)
-> (Product Var CType -> Type)
-> Either (Product Var CType) (Product Var CType)
-> Type
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
      (\Product Var CType
x -> (Product Var CType -> Type)
-> (Product Var CType -> Type)
-> Either (Product Var CType) (Product Var CType)
-> Type
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
               -- x neg, y neg
               (\Product Var CType
y -> let r :: Type
r = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon [Product Var CType -> Type
reifyProduct Product Var CType
x
                                                         ,Product Var CType -> Type
reifyProduct Product Var CType
y]
                      in  TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon [Integer -> Type
mkNumLitTy Integer
0, Type
r])
               -- x neg, y pos
               (\Product Var CType
y -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon [Product Var CType -> Type
reifyProduct Product Var CType
y, Product Var CType -> Type
reifyProduct Product Var CType
x])
               Either (Product Var CType) (Product Var CType)
p2)
      (\Product Var CType
x -> (Product Var CType -> Type)
-> (Product Var CType -> Type)
-> Either (Product Var CType) (Product Var CType)
-> Type
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
               -- x pos, y neg
               (\Product Var CType
y -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon [Product Var CType -> Type
reifyProduct Product Var CType
x, Product Var CType -> Type
reifyProduct Product Var CType
y])
               -- x pos, y pos
               (\Product Var CType
y -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatAddTyCon [Product Var CType -> Type
reifyProduct Product Var CType
x, Product Var CType -> Type
reifyProduct Product Var CType
y])
               Either (Product Var CType) (Product Var CType)
p2)
      Either (Product Var CType) (Product Var CType)
p1


    combineP (Either (Product Var CType) (Product Var CType)
p:[Either (Product Var CType) (Product Var CType)]
ps)  = let es :: Type
es = [Either (Product Var CType) (Product Var CType)] -> Type
combineP [Either (Product Var CType) (Product Var CType)]
ps
                       in  (Product Var CType -> Type)
-> (Product Var CType -> Type)
-> Either (Product Var CType) (Product Var CType)
-> Type
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\Product Var CType
x -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon
                                                    [Type
es, Product Var CType -> Type
reifyProduct Product Var CType
x])
                                  (\Product Var CType
x -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatAddTyCon
                                                   [Product Var CType -> Type
reifyProduct Product Var CType
x, Type
es])
                                  Either (Product Var CType) (Product Var CType)
p

reifyProduct :: CoreProduct -> Type
reifyProduct :: Product Var CType -> Type
reifyProduct (P [Symbol Var CType]
ps) =
    let ps' :: [Type]
ps' = (Either (Symbol Var CType) (CoreSOP, [Product Var CType]) -> Type)
-> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
-> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Either (Symbol Var CType) (CoreSOP, [Product Var CType]) -> Type
reifySymbol ((Symbol Var CType
 -> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
 -> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])])
-> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
-> [Symbol Var CType]
-> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Symbol Var CType
-> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
-> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
mergeExp [] [Symbol Var CType]
ps)
    in  (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Type
t1 Type
t2 -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatMulTyCon [Type
t1,Type
t2]) ([Type] -> Type
forall a. [a] -> a
head [Type]
ps') ([Type] -> [Type]
forall a. [a] -> [a]
tail [Type]
ps')
  where
    -- "2 ^ -1 * 2 ^ a" must be merged into "2 ^ (a-1)", otherwise GHC barfs
    -- at the "2 ^ -1" because of the negative exponent.
    mergeExp :: CoreSymbol -> [Either CoreSymbol (CoreSOP,[CoreProduct])]
                           -> [Either CoreSymbol (CoreSOP,[CoreProduct])]
    mergeExp :: Symbol Var CType
-> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
-> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
mergeExp (E CoreSOP
s Product Var CType
p)   []     = [(CoreSOP, [Product Var CType])
-> Either (Symbol Var CType) (CoreSOP, [Product Var CType])
forall a b. b -> Either a b
Right (CoreSOP
s,[Product Var CType
p])]
    mergeExp (E CoreSOP
s1 Product Var CType
p1) (Either (Symbol Var CType) (CoreSOP, [Product Var CType])
y:[Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
ys)
      | Right (CoreSOP
s2,[Product Var CType]
p2) <- Either (Symbol Var CType) (CoreSOP, [Product Var CType])
y
      , CoreSOP
s1 CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
== CoreSOP
s2
      = (CoreSOP, [Product Var CType])
-> Either (Symbol Var CType) (CoreSOP, [Product Var CType])
forall a b. b -> Either a b
Right (CoreSOP
s1,(Product Var CType
p1Product Var CType -> [Product Var CType] -> [Product Var CType]
forall a. a -> [a] -> [a]
:[Product Var CType]
p2)) Either (Symbol Var CType) (CoreSOP, [Product Var CType])
-> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
-> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
forall a. a -> [a] -> [a]
: [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
ys
      | Bool
otherwise
      = (CoreSOP, [Product Var CType])
-> Either (Symbol Var CType) (CoreSOP, [Product Var CType])
forall a b. b -> Either a b
Right (CoreSOP
s1,[Product Var CType
p1]) Either (Symbol Var CType) (CoreSOP, [Product Var CType])
-> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
-> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
forall a. a -> [a] -> [a]
: Either (Symbol Var CType) (CoreSOP, [Product Var CType])
y Either (Symbol Var CType) (CoreSOP, [Product Var CType])
-> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
-> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
forall a. a -> [a] -> [a]
: [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
ys
    mergeExp Symbol Var CType
x [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
ys = Symbol Var CType
-> Either (Symbol Var CType) (CoreSOP, [Product Var CType])
forall a b. a -> Either a b
Left Symbol Var CType
x Either (Symbol Var CType) (CoreSOP, [Product Var CType])
-> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
-> [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
forall a. a -> [a] -> [a]
: [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
ys

reifySymbol :: Either CoreSymbol (CoreSOP,[CoreProduct]) -> Type
reifySymbol :: Either (Symbol Var CType) (CoreSOP, [Product Var CType]) -> Type
reifySymbol (Left (I Integer
i)  )  = Integer -> Type
mkNumLitTy Integer
i
reifySymbol (Left (C CType
c)  )  = CType -> Type
unCType CType
c
reifySymbol (Left (V Var
v)  )  = Var -> Type
mkTyVarTy Var
v
reifySymbol (Left (E CoreSOP
s Product Var CType
p))  = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatExpTyCon [CoreSOP -> Type
reifySOP CoreSOP
s,Product Var CType -> Type
reifyProduct Product Var CType
p]
reifySymbol (Right (CoreSOP
s1,[Product Var CType]
s2)) = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatExpTyCon
                                         [CoreSOP -> Type
reifySOP CoreSOP
s1
                                         ,CoreSOP -> Type
reifySOP ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType]
s2)
                                         ]

-- | Subtract an inequality, in order to either:
--
-- * See if the smallest solution is a natural number
-- * Cancel sums, i.e. monotonicity of addition
--
-- @
-- subtractIneq (2*y <=? 3*x ~ True)  = (-2*y + 3*x)
-- subtractIneq (2*y <=? 3*x ~ False) = (-3*x + (-1) + 2*y)
-- @
subtractIneq
  :: (CoreSOP, CoreSOP, Bool)
  -> CoreSOP
subtractIneq :: (CoreSOP, CoreSOP, Bool) -> CoreSOP
subtractIneq (CoreSOP
x,CoreSOP
y,Bool
isLE)
  | Bool
isLE
  = CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd CoreSOP
y (CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I (-Integer
1)]]) CoreSOP
x)
  | Bool
otherwise
  = CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd CoreSOP
x (CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I (-Integer
1)]]) (CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd CoreSOP
y ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
1]])))

-- | Try to reverse the process of 'subtractIneq'
--
-- E.g.
--
-- @
-- subtractIneq (2*y <=? 3*x ~ True) = (-2*y + 3*x)
-- sopToIneq (-2*y+3*x) = Just (2*x <=? 3*x ~ True)
-- @
sopToIneq
  :: CoreSOP
  -> Maybe Ineq
sopToIneq :: CoreSOP -> Maybe (CoreSOP, CoreSOP, Bool)
sopToIneq (S [P ((I Integer
i):[Symbol Var CType]
l),Product Var CType
r])
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
  = (CoreSOP, CoreSOP, Bool) -> Maybe (CoreSOP, CoreSOP, Bool)
forall a. a -> Maybe a
Just (CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I (Integer -> Integer
forall a. Num a => a -> a
negate Integer
i)]]) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
l]),[Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
r],Bool
True)
sopToIneq (S [Product Var CType
r,P ((I Integer
i:[Symbol Var CType]
l))])
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
  = (CoreSOP, CoreSOP, Bool) -> Maybe (CoreSOP, CoreSOP, Bool)
forall a. a -> Maybe a
Just (CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I (Integer -> Integer
forall a. Num a => a -> a
negate Integer
i)]]) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
l]),[Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
r],Bool
True)
sopToIneq CoreSOP
_ = Maybe (CoreSOP, CoreSOP, Bool)
forall a. Maybe a
Nothing

-- | Give the smallest solution for an inequality
ineqToSubst
  :: Ineq
  -> Maybe CoreUnify
ineqToSubst :: (CoreSOP, CoreSOP, Bool) -> Maybe CoreUnify
ineqToSubst (CoreSOP
x,S [P [V Var
v]],Bool
True)
  = CoreUnify -> Maybe CoreUnify
forall a. a -> Maybe a
Just (Var -> CoreSOP -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem Var
v CoreSOP
x)
ineqToSubst (CoreSOP, CoreSOP, Bool)
_
  = Maybe CoreUnify
forall a. Maybe a
Nothing

subtractionToPred
  :: (Type,Type)
  -> (PredType, Kind)
subtractionToPred :: (Type, Type) -> (Type, Type)
subtractionToPred (Type
x,Type
y) =
  (Type -> Type -> Type
mkPrimEqPred (TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatLeqTyCon [Type
y,Type
x])
                (TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedTrueDataCon [])
  ,Type
boolTy)

-- | A substitution is essentially a list of (variable, 'SOP') pairs,
-- but we keep the original 'Ct' that lead to the substitution being
-- made, for use when turning the substitution back into constraints.
type CoreUnify = UnifyItem TyVar CType

data UnifyItem v c = SubstItem { UnifyItem v c -> v
siVar :: v
                               , UnifyItem v c -> SOP v c
siSOP :: SOP v c
                               }
                   | UnifyItem { UnifyItem v c -> SOP v c
siLHS :: SOP v c
                               , UnifyItem v c -> SOP v c
siRHS :: SOP v c
                               }
  deriving UnifyItem v c -> UnifyItem v c -> Bool
(UnifyItem v c -> UnifyItem v c -> Bool)
-> (UnifyItem v c -> UnifyItem v c -> Bool) -> Eq (UnifyItem v c)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall v c. (Eq v, Eq c) => UnifyItem v c -> UnifyItem v c -> Bool
/= :: UnifyItem v c -> UnifyItem v c -> Bool
$c/= :: forall v c. (Eq v, Eq c) => UnifyItem v c -> UnifyItem v c -> Bool
== :: UnifyItem v c -> UnifyItem v c -> Bool
$c== :: forall v c. (Eq v, Eq c) => UnifyItem v c -> UnifyItem v c -> Bool
Eq

instance (Outputable v, Outputable c) => Outputable (UnifyItem v c) where
  ppr :: UnifyItem v c -> SDoc
ppr (SubstItem {v
SOP v c
siSOP :: SOP v c
siVar :: v
siSOP :: forall v c. UnifyItem v c -> SOP v c
siVar :: forall v c. UnifyItem v c -> v
..}) = v -> SDoc
forall a. Outputable a => a -> SDoc
ppr v
siVar SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
" := " SDoc -> SDoc -> SDoc
<+> SOP v c -> SDoc
forall a. Outputable a => a -> SDoc
ppr SOP v c
siSOP
  ppr (UnifyItem {SOP v c
siRHS :: SOP v c
siLHS :: SOP v c
siRHS :: forall v c. UnifyItem v c -> SOP v c
siLHS :: forall v c. UnifyItem v c -> SOP v c
..}) = SOP v c -> SDoc
forall a. Outputable a => a -> SDoc
ppr SOP v c
siLHS SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
" :~ " SDoc -> SDoc -> SDoc
<+> SOP v c -> SDoc
forall a. Outputable a => a -> SDoc
ppr SOP v c
siRHS

-- | Apply a substitution to a single normalised 'SOP' term
substsSOP :: (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP :: [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP []                   SOP v c
u = SOP v c
u
substsSOP ((SubstItem {v
SOP v c
siSOP :: SOP v c
siVar :: v
siSOP :: forall v c. UnifyItem v c -> SOP v c
siVar :: forall v c. UnifyItem v c -> v
..}):[UnifyItem v c]
s) SOP v c
u = [UnifyItem v c] -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [UnifyItem v c]
s (v -> SOP v c -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c
substSOP v
siVar SOP v c
siSOP SOP v c
u)
substsSOP ((UnifyItem {}):[UnifyItem v c]
s)   SOP v c
u = [UnifyItem v c] -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [UnifyItem v c]
s SOP v c
u

substSOP :: (Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c
substSOP :: v -> SOP v c -> SOP v c -> SOP v c
substSOP v
tv SOP v c
e = (SOP v c -> SOP v c -> SOP v c) -> [SOP v c] -> SOP v c
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 SOP v c -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd ([SOP v c] -> SOP v c)
-> (SOP v c -> [SOP v c]) -> SOP v c -> SOP v c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Product v c -> SOP v c) -> [Product v c] -> [SOP v c]
forall a b. (a -> b) -> [a] -> [b]
map (v -> SOP v c -> Product v c -> SOP v c
forall v c.
(Ord v, Ord c) =>
v -> SOP v c -> Product v c -> SOP v c
substProduct v
tv SOP v c
e) ([Product v c] -> [SOP v c])
-> (SOP v c -> [Product v c]) -> SOP v c -> [SOP v c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SOP v c -> [Product v c]
forall v c. SOP v c -> [Product v c]
unS

substProduct :: (Ord v, Ord c) => v -> SOP v c -> Product v c -> SOP v c
substProduct :: v -> SOP v c -> Product v c -> SOP v c
substProduct v
tv SOP v c
e = (SOP v c -> SOP v c -> SOP v c) -> [SOP v c] -> SOP v c
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 SOP v c -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul ([SOP v c] -> SOP v c)
-> (Product v c -> [SOP v c]) -> Product v c -> SOP v c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol v c -> SOP v c) -> [Symbol v c] -> [SOP v c]
forall a b. (a -> b) -> [a] -> [b]
map (v -> SOP v c -> Symbol v c -> SOP v c
forall v c. (Ord v, Ord c) => v -> SOP v c -> Symbol v c -> SOP v c
substSymbol v
tv SOP v c
e) ([Symbol v c] -> [SOP v c])
-> (Product v c -> [Symbol v c]) -> Product v c -> [SOP v c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product v c -> [Symbol v c]
forall v c. Product v c -> [Symbol v c]
unP

substSymbol :: (Ord v, Ord c) => v -> SOP v c -> Symbol v c -> SOP v c
substSymbol :: v -> SOP v c -> Symbol v c -> SOP v c
substSymbol v
_  SOP v c
_ s :: Symbol v c
s@(I Integer
_) = [Product v c] -> SOP v c
forall v c. [Product v c] -> SOP v c
S [[Symbol v c] -> Product v c
forall v c. [Symbol v c] -> Product v c
P [Symbol v c
s]]
substSymbol v
_  SOP v c
_ s :: Symbol v c
s@(C c
_) = [Product v c] -> SOP v c
forall v c. [Product v c] -> SOP v c
S [[Symbol v c] -> Product v c
forall v c. [Symbol v c] -> Product v c
P [Symbol v c
s]]
substSymbol v
tv SOP v c
e (V v
tv')
  | v
tv v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
tv'            = SOP v c
e
  | Bool
otherwise            = [Product v c] -> SOP v c
forall v c. [Product v c] -> SOP v c
S [[Symbol v c] -> Product v c
forall v c. [Symbol v c] -> Product v c
P [v -> Symbol v c
forall v c. v -> Symbol v c
V v
tv']]
substSymbol v
tv SOP v c
e (E SOP v c
s Product v c
p) = SOP v c -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
normaliseExp (v -> SOP v c -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c
substSOP v
tv SOP v c
e SOP v c
s) (v -> SOP v c -> Product v c -> SOP v c
forall v c.
(Ord v, Ord c) =>
v -> SOP v c -> Product v c -> SOP v c
substProduct v
tv SOP v c
e Product v c
p)

-- | Apply a substitution to a substitution
substsSubst :: (Ord v, Ord c) => [UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c]
substsSubst :: [UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c]
substsSubst [UnifyItem v c]
s = (UnifyItem v c -> UnifyItem v c)
-> [UnifyItem v c] -> [UnifyItem v c]
forall a b. (a -> b) -> [a] -> [b]
map UnifyItem v c -> UnifyItem v c
subt
  where
    subt :: UnifyItem v c -> UnifyItem v c
subt si :: UnifyItem v c
si@(SubstItem {v
SOP v c
siSOP :: SOP v c
siVar :: v
siSOP :: forall v c. UnifyItem v c -> SOP v c
siVar :: forall v c. UnifyItem v c -> v
..}) = UnifyItem v c
si {siSOP :: SOP v c
siSOP = [UnifyItem v c] -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [UnifyItem v c]
s SOP v c
siSOP}
    subt si :: UnifyItem v c
si@(UnifyItem {SOP v c
siRHS :: SOP v c
siLHS :: SOP v c
siRHS :: forall v c. UnifyItem v c -> SOP v c
siLHS :: forall v c. UnifyItem v c -> SOP v c
..}) = UnifyItem v c
si {siLHS :: SOP v c
siLHS = [UnifyItem v c] -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [UnifyItem v c]
s SOP v c
siLHS, siRHS :: SOP v c
siRHS = [UnifyItem v c] -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [UnifyItem v c]
s SOP v c
siRHS}
{-# INLINEABLE substsSubst #-}

-- | Result of comparing two 'SOP' terms, returning a potential substitution
-- list under which the two terms are equal.
data UnifyResult
  = Win              -- ^ Two terms are equal
  | Lose             -- ^ Two terms are /not/ equal
  | Draw [CoreUnify] -- ^ Two terms are only equal if the given substitution holds

instance Outputable UnifyResult where
  ppr :: UnifyResult -> SDoc
ppr UnifyResult
Win          = String -> SDoc
text String
"Win"
  ppr (Draw [CoreUnify]
subst) = String -> SDoc
text String
"Draw" SDoc -> SDoc -> SDoc
<+> [CoreUnify] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [CoreUnify]
subst
  ppr UnifyResult
Lose         = String -> SDoc
text String
"Lose"

-- | Given two 'SOP's @u@ and @v@, when their free variables ('fvSOP') are the
-- same, then we 'Win' if @u@ and @v@ are equal, and 'Lose' otherwise.
--
-- If @u@ and @v@ do not have the same free variables, we result in a 'Draw',
-- ware @u@ and @v@ are only equal when the returned 'CoreSubst' holds.
unifyNats :: Ct -> CoreSOP -> CoreSOP -> TcPluginM UnifyResult
unifyNats :: Ct -> CoreSOP -> CoreSOP -> TcPluginM UnifyResult
unifyNats Ct
ct CoreSOP
u CoreSOP
v = do
  String -> SDoc -> TcPluginM ()
tcPluginTrace String
"unifyNats" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct SDoc -> SDoc -> SDoc
$$ CoreSOP -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreSOP
u SDoc -> SDoc -> SDoc
$$ CoreSOP -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreSOP
v)
  UnifyResult -> TcPluginM UnifyResult
forall (m :: * -> *) a. Monad m => a -> m a
return (Ct -> CoreSOP -> CoreSOP -> UnifyResult
unifyNats' Ct
ct CoreSOP
u CoreSOP
v)

unifyNats' :: Ct -> CoreSOP -> CoreSOP -> UnifyResult
unifyNats' :: Ct -> CoreSOP -> CoreSOP -> UnifyResult
unifyNats' Ct
ct CoreSOP
u CoreSOP
v
  = if CoreSOP -> CoreSOP -> Bool
eqFV CoreSOP
u CoreSOP
v
       then if CoreSOP -> Bool
containsConstants CoreSOP
u Bool -> Bool -> Bool
|| CoreSOP -> Bool
containsConstants CoreSOP
v
               then if CoreSOP
u CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
== CoreSOP
v
                       then UnifyResult
Win
                       else [CoreUnify] -> UnifyResult
Draw ((CoreUnify -> Bool) -> [CoreUnify] -> [CoreUnify]
forall a. (a -> Bool) -> [a] -> [a]
filter CoreUnify -> Bool
diffFromConstraint (Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers Ct
ct CoreSOP
u CoreSOP
v))
               else if CoreSOP
u CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
== CoreSOP
v
                       then UnifyResult
Win
                       else UnifyResult
Lose
       else [CoreUnify] -> UnifyResult
Draw ((CoreUnify -> Bool) -> [CoreUnify] -> [CoreUnify]
forall a. (a -> Bool) -> [a] -> [a]
filter CoreUnify -> Bool
diffFromConstraint (Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers Ct
ct CoreSOP
u CoreSOP
v))
  where
    -- A unifier is only a unifier if differs from the original constraint
    diffFromConstraint :: CoreUnify -> Bool
diffFromConstraint (UnifyItem CoreSOP
x CoreSOP
y) = Bool -> Bool
not (CoreSOP
x CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
== CoreSOP
u Bool -> Bool -> Bool
&& CoreSOP
y CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
== CoreSOP
v)
    diffFromConstraint CoreUnify
_               = Bool
True

-- | Find unifiers for two SOP terms
--
-- Can find the following unifiers:
--
-- @
-- t ~ a + b          ==>  [t := a + b]
-- a + b ~ t          ==>  [t := a + b]
-- (a + c) ~ (b + c)  ==>  \[a := b\]
-- (2*a) ~ (2*b)      ==>  [a := b]
-- (2 + a) ~ 5        ==>  [a := 3]
-- (i * a) ~ j        ==>  [a := div j i], when (mod j i == 0)
-- @
--
-- However, given a wanted:
--
-- @
-- [W] t ~ a + b
-- @
--
-- this function returns @[]@, or otherwise we \"solve\" the constraint by
-- finding a unifier equal to the constraint.
--
-- However, given a wanted:
--
-- @
-- [W] (a + c) ~ (b + c)
-- @
--
-- we do return the unifier:
--
-- @
-- [a := b]
-- @
unifiers :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers Ct
ct u :: CoreSOP
u@(S [P [V Var
x]]) CoreSOP
v
  = 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
_
        | Type -> CType
CType (CoreSOP -> Type
reifySOP CoreSOP
u) CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
/= Type -> CType
CType Type
t1 Bool -> Bool -> Bool
|| CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct) -> [Var -> CoreSOP -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem Var
x CoreSOP
v]
      Pred
_ -> []
unifiers Ct
ct CoreSOP
u v :: CoreSOP
v@(S [P [V Var
x]])
  = 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
_ Type
t2
        | Type -> CType
CType (CoreSOP -> Type
reifySOP CoreSOP
v) CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
/= Type -> CType
CType Type
t2 Bool -> Bool -> Bool
|| CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct) -> [Var -> CoreSOP -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem Var
x CoreSOP
u]
      Pred
_ -> []
unifiers Ct
ct u :: CoreSOP
u@(S [P [C CType
_]]) CoreSOP
v
  = 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
        | Type -> CType
CType (CoreSOP -> Type
reifySOP CoreSOP
u) CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
/= Type -> CType
CType Type
t1 Bool -> Bool -> Bool
|| Type -> CType
CType (CoreSOP -> Type
reifySOP CoreSOP
v) CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
/= Type -> CType
CType Type
t2 -> [CoreSOP -> CoreSOP -> CoreUnify
forall v c. SOP v c -> SOP v c -> UnifyItem v c
UnifyItem CoreSOP
u CoreSOP
v]
      Pred
_ -> []
unifiers Ct
ct CoreSOP
u v :: CoreSOP
v@(S [P [C CType
_]])
  = 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
        | Type -> CType
CType (CoreSOP -> Type
reifySOP CoreSOP
u) CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
/= Type -> CType
CType Type
t1 Bool -> Bool -> Bool
|| Type -> CType
CType (CoreSOP -> Type
reifySOP CoreSOP
v) CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
/= Type -> CType
CType Type
t2 -> [CoreSOP -> CoreSOP -> CoreUnify
forall v c. SOP v c -> SOP v c -> UnifyItem v c
UnifyItem CoreSOP
u CoreSOP
v]
      Pred
_ -> []
unifiers Ct
ct CoreSOP
u CoreSOP
v             = Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' Ct
ct CoreSOP
u CoreSOP
v

unifiers' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' Ct
_ct (S [P [V Var
x]]) (S [])        = [Var -> CoreSOP -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem Var
x ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
0]])]
unifiers' Ct
_ct (S [])        (S [P [V Var
x]]) = [Var -> CoreSOP -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem Var
x ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
0]])]

unifiers' Ct
_ct (S [P [V Var
x]]) CoreSOP
s             = [Var -> CoreSOP -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem Var
x CoreSOP
s]
unifiers' Ct
_ct CoreSOP
s             (S [P [V Var
x]]) = [Var -> CoreSOP -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem Var
x CoreSOP
s]

unifiers' Ct
_ct s1 :: CoreSOP
s1@(S [P [C CType
_]]) CoreSOP
s2               = [CoreSOP -> CoreSOP -> CoreUnify
forall v c. SOP v c -> SOP v c -> UnifyItem v c
UnifyItem CoreSOP
s1 CoreSOP
s2]
unifiers' Ct
_ct CoreSOP
s1               s2 :: CoreSOP
s2@(S [P [C CType
_]]) = [CoreSOP -> CoreSOP -> CoreUnify
forall v c. SOP v c -> SOP v c -> UnifyItem v c
UnifyItem CoreSOP
s1 CoreSOP
s2]


-- (z ^ a) ~ (z ^ b) ==> [a := b]
unifiers' Ct
ct (S [P [E CoreSOP
s1 Product Var CType
p1]]) (S [P [E CoreSOP
s2 Product Var CType
p2]])
  | CoreSOP
s1 CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
== CoreSOP
s2 = Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
p1]) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
p2])

-- (2*e ^ d) ~ (2*e*a*c) ==> [a*c := 2*e ^ (d-1)]
unifiers' Ct
ct (S [P [E (S [P [Symbol Var CType]
s1]) Product Var CType
p1]]) (S [P [Symbol Var CType]
p2])
  | (Symbol Var CType -> Bool) -> [Symbol Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Symbol Var CType -> [Symbol Var CType] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol Var CType]
p2) [Symbol Var CType]
s1
  = let base :: [Symbol Var CType]
base = [Symbol Var CType] -> [Symbol Var CType] -> [Symbol Var CType]
forall a. Eq a => [a] -> [a] -> [a]
intersect [Symbol Var CType]
s1 [Symbol Var CType]
p2
        diff :: [Symbol Var CType]
diff = [Symbol Var CType]
p2 [Symbol Var CType] -> [Symbol Var CType] -> [Symbol Var CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol Var CType]
s1
    in  Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
diff]) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [CoreSOP -> Product Var CType -> Symbol Var CType
forall v c. SOP v c -> Product v c -> Symbol v c
E ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
base]) ([Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I (-Integer
1)]),CoreSOP -> Product Var CType -> Symbol Var CType
forall v c. SOP v c -> Product v c -> Symbol v c
E ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
base]) Product Var CType
p1]])

unifiers' Ct
ct (S [P [Symbol Var CType]
p2]) (S [P [E (S [P [Symbol Var CType]
s1]) Product Var CType
p1]])
  | (Symbol Var CType -> Bool) -> [Symbol Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Symbol Var CType -> [Symbol Var CType] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol Var CType]
p2) [Symbol Var CType]
s1
  = let base :: [Symbol Var CType]
base = [Symbol Var CType] -> [Symbol Var CType] -> [Symbol Var CType]
forall a. Eq a => [a] -> [a] -> [a]
intersect [Symbol Var CType]
s1 [Symbol Var CType]
p2
        diff :: [Symbol Var CType]
diff = [Symbol Var CType]
p2 [Symbol Var CType] -> [Symbol Var CType] -> [Symbol Var CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol Var CType]
s1
    in  Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [CoreSOP -> Product Var CType -> Symbol Var CType
forall v c. SOP v c -> Product v c -> Symbol v c
E ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
base]) ([Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I (-Integer
1)]),CoreSOP -> Product Var CType -> Symbol Var CType
forall v c. SOP v c -> Product v c -> Symbol v c
E ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
base]) Product Var CType
p1]]) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
diff])

-- (i ^ a) ~ j ==> [a := round (logBase i j)], when `i` and `j` are integers,
-- and `ceiling (logBase i j) == floor (logBase i j)`
unifiers' Ct
ct (S [P [E (S [P [I Integer
i]]) Product Var CType
p]]) (S [P [I Integer
j]])
  = case Integer -> Integer -> Maybe Integer
integerLogBase Integer
i Integer
j of
      Just Integer
k  -> Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
p]) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
k]])
      Maybe Integer
Nothing -> []

unifiers' Ct
ct (S [P [I Integer
j]]) (S [P [E (S [P [I Integer
i]]) Product Var CType
p]])
  = case Integer -> Integer -> Maybe Integer
integerLogBase Integer
i Integer
j of
      Just Integer
k  -> Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
p]) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
k]])
      Maybe Integer
Nothing -> []

-- a^d * a^e ~ a^c ==> [c := d + e]
unifiers' Ct
ct (S [P [E CoreSOP
s1 Product Var CType
p1]]) (S [Product Var CType
p2]) = case Product Var CType -> Maybe ([CoreSOP], [Product Var CType])
collectBases Product Var CType
p2 of
  Just (CoreSOP
b:[CoreSOP]
bs,[Product Var CType]
ps) | (CoreSOP -> Bool) -> [CoreSOP] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
== CoreSOP
s1) (CoreSOP
bCoreSOP -> [CoreSOP] -> [CoreSOP]
forall a. a -> [a] -> [a]
:[CoreSOP]
bs) ->
    Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
p1]) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType]
ps)
  Maybe ([CoreSOP], [Product Var CType])
_ -> []

unifiers' Ct
ct (S [Product Var CType
p2]) (S [P [E CoreSOP
s1 Product Var CType
p1]]) = case Product Var CType -> Maybe ([CoreSOP], [Product Var CType])
collectBases Product Var CType
p2 of
  Just (CoreSOP
b:[CoreSOP]
bs,[Product Var CType]
ps) | (CoreSOP -> Bool) -> [CoreSOP] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
== CoreSOP
s1) (CoreSOP
bCoreSOP -> [CoreSOP] -> [CoreSOP]
forall a. a -> [a] -> [a]
:[CoreSOP]
bs) ->
    Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType]
ps) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
p1])
  Maybe ([CoreSOP], [Product Var CType])
_ -> []

-- (i * a) ~ j ==> [a := div j i]
-- Where 'a' is a variable, 'i' and 'j' are integer literals, and j `mod` i == 0
unifiers' Ct
ct (S [P ((I Integer
i):[Symbol Var CType]
ps)]) (S [P [I Integer
j]]) =
  case Integer -> Integer -> Maybe Integer
safeDiv Integer
j Integer
i of
    Just Integer
k -> Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
ps]) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
k]])
    Maybe Integer
_      -> []

unifiers' Ct
ct (S [P [I Integer
j]]) (S [P ((I Integer
i):[Symbol Var CType]
ps)]) =
  case Integer -> Integer -> Maybe Integer
safeDiv Integer
j Integer
i of
    Just Integer
k -> Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
ps]) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
k]])
    Maybe Integer
_      -> []

-- (2*a) ~ (2*b) ==> [a := b]
-- unifiers' ct (S [P (p:ps1)]) (S [P (p':ps2)])
--     | p == p'   = unifiers' ct (S [P ps1]) (S [P ps2])
--     | otherwise = []
unifiers' Ct
ct (S [P [Symbol Var CType]
ps1]) (S [P [Symbol Var CType]
ps2])
    | [Symbol Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol Var CType]
psx  = []
    | Bool
otherwise = Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
ps1'']) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
ps2''])
  where
    ps1' :: [Symbol Var CType]
ps1'  = [Symbol Var CType]
ps1 [Symbol Var CType] -> [Symbol Var CType] -> [Symbol Var CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol Var CType]
psx
    ps2' :: [Symbol Var CType]
ps2'  = [Symbol Var CType]
ps2 [Symbol Var CType] -> [Symbol Var CType] -> [Symbol Var CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol Var CType]
psx
    ps1'' :: [Symbol Var CType]
ps1'' | [Symbol Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol Var CType]
ps1' = [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
1]
          | Bool
otherwise = [Symbol Var CType]
ps1'
    ps2'' :: [Symbol Var CType]
ps2'' | [Symbol Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol Var CType]
ps2' = [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
1]
          | Bool
otherwise = [Symbol Var CType]
ps2'
    psx :: [Symbol Var CType]
psx  = [Symbol Var CType] -> [Symbol Var CType] -> [Symbol Var CType]
forall a. Eq a => [a] -> [a] -> [a]
intersect [Symbol Var CType]
ps1 [Symbol Var CType]
ps2

-- (2 + a) ~ 5 ==> [a := 3]
unifiers' Ct
ct (S ((P [I Integer
i]):[Product Var CType]
ps1)) (S ((P [I Integer
j]):[Product Var CType]
ps2))
    | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
j     = Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType]
ps1) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S (([Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I (Integer
jInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
i)])Product Var CType -> [Product Var CType] -> [Product Var CType]
forall a. a -> [a] -> [a]
:[Product Var CType]
ps2))
    | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
j     = Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S (([Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
j)])Product Var CType -> [Product Var CType] -> [Product Var CType]
forall a. a -> [a] -> [a]
:[Product Var CType]
ps1)) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType]
ps2)

-- (a + c) ~ (b + c) ==> [a := b]
unifiers' Ct
ct s1 :: CoreSOP
s1@(S [Product Var CType]
ps1) s2 :: CoreSOP
s2@(S [Product Var CType]
ps2) = case CoreSOP -> Maybe (CoreSOP, CoreSOP, Bool)
sopToIneq CoreSOP
k1 of
  Just (CoreSOP
s1',CoreSOP
s2',Bool
_)
    | CoreSOP
s1' CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
/= CoreSOP
s1 Bool -> Bool -> Bool
|| CoreSOP
s2' CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
/= CoreSOP
s1
    , Bool
-> ((Bool, Set CType) -> Bool) -> Maybe (Bool, Set CType) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ((Bool -> Bool -> Bool) -> (Bool, Bool) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Bool -> Bool -> Bool
(&&) ((Bool, Bool) -> Bool)
-> ((Bool, Set CType) -> (Bool, Bool)) -> (Bool, Set CType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set CType -> Bool) -> (Bool, Set CType) -> (Bool, Bool)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Set CType -> Bool
forall a. Set a -> Bool
Set.null) (WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural CoreSOP
s1'))
    , Bool
-> ((Bool, Set CType) -> Bool) -> Maybe (Bool, Set CType) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ((Bool -> Bool -> Bool) -> (Bool, Bool) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Bool -> Bool -> Bool
(&&) ((Bool, Bool) -> Bool)
-> ((Bool, Set CType) -> (Bool, Bool)) -> (Bool, Set CType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set CType -> Bool) -> (Bool, Set CType) -> (Bool, Bool)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Set CType -> Bool
forall a. Set a -> Bool
Set.null) (WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural CoreSOP
s2'))
    -> Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' Ct
ct CoreSOP
s1' CoreSOP
s2'
  Maybe (CoreSOP, CoreSOP, Bool)
_ | [Product Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product Var CType]
psx
    , [Product Var CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Product Var CType]
ps1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Product Var CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Product Var CType]
ps2
    -> case [CoreUnify] -> [CoreUnify]
forall a. Eq a => [a] -> [a]
nub ([[CoreUnify]] -> [CoreUnify]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((Product Var CType -> Product Var CType -> [CoreUnify])
-> [Product Var CType] -> [Product Var CType] -> [[CoreUnify]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Product Var CType
x Product Var CType
y -> Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
x]) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
y])) [Product Var CType]
ps1 [Product Var CType]
ps2)) of
        []                             -> Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers'' Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType]
ps1) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType]
ps2)
        [CoreUnify
k] | [Product Var CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Product Var CType]
ps1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Product Var CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Product Var CType]
ps2 -> [CoreUnify
k]
        [CoreUnify]
_                              -> []
    | [Product Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product Var CType]
psx
    , CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct)
    -> Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers'' Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType]
ps1) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType]
ps2)
    | [Product Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product Var CType]
psx
    -> []
  Maybe (CoreSOP, CoreSOP, Bool)
_ -> Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' Ct
ct ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType]
ps1'') ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType]
ps2'')
  where
    k1 :: CoreSOP
k1 = (CoreSOP, CoreSOP, Bool) -> CoreSOP
subtractIneq (CoreSOP
s1,CoreSOP
s2,Bool
True)
    ps1' :: [Product Var CType]
ps1'  = [Product Var CType]
ps1 [Product Var CType] -> [Product Var CType] -> [Product Var CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Product Var CType]
psx
    ps2' :: [Product Var CType]
ps2'  = [Product Var CType]
ps2 [Product Var CType] -> [Product Var CType] -> [Product Var CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Product Var CType]
psx
    ps1'' :: [Product Var CType]
ps1'' | [Product Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product Var CType]
ps1' = [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
0]]
          | Bool
otherwise = [Product Var CType]
ps1'
    ps2'' :: [Product Var CType]
ps2'' | [Product Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product Var CType]
ps2' = [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
0]]
          | Bool
otherwise = [Product Var CType]
ps2'
    psx :: [Product Var CType]
psx = [Product Var CType] -> [Product Var CType] -> [Product Var CType]
forall a. Eq a => [a] -> [a] -> [a]
intersect [Product Var CType]
ps1 [Product Var CType]
ps2

unifiers'' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers'' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers'' Ct
ct (S [P [I Integer
i],P [V Var
v]]) CoreSOP
s2
  | CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct) = [Var -> CoreSOP -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem Var
v (CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd CoreSOP
s2 ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I (Integer -> Integer
forall a. Num a => a -> a
negate Integer
i)]]))]
unifiers'' Ct
ct CoreSOP
s1 (S [P [I Integer
i],P [V Var
v]])
  | CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct) = [Var -> CoreSOP -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem Var
v (CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd CoreSOP
s1 ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I (Integer -> Integer
forall a. Num a => a -> a
negate Integer
i)]]))]
unifiers'' Ct
_ CoreSOP
_ CoreSOP
_ = []

collectBases :: CoreProduct -> Maybe ([CoreSOP],[CoreProduct])
collectBases :: Product Var CType -> Maybe ([CoreSOP], [Product Var CType])
collectBases = ([(CoreSOP, Product Var CType)]
 -> ([CoreSOP], [Product Var CType]))
-> Maybe [(CoreSOP, Product Var CType)]
-> Maybe ([CoreSOP], [Product Var CType])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(CoreSOP, Product Var CType)] -> ([CoreSOP], [Product Var CType])
forall a b. [(a, b)] -> ([a], [b])
unzip (Maybe [(CoreSOP, Product Var CType)]
 -> Maybe ([CoreSOP], [Product Var CType]))
-> (Product Var CType -> Maybe [(CoreSOP, Product Var CType)])
-> Product Var CType
-> Maybe ([CoreSOP], [Product Var CType])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol Var CType -> Maybe (CoreSOP, Product Var CType))
-> [Symbol Var CType] -> Maybe [(CoreSOP, Product Var CType)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Symbol Var CType -> Maybe (CoreSOP, Product Var CType)
forall v c. Symbol v c -> Maybe (SOP v c, Product v c)
go ([Symbol Var CType] -> Maybe [(CoreSOP, Product Var CType)])
-> (Product Var CType -> [Symbol Var CType])
-> Product Var CType
-> Maybe [(CoreSOP, Product Var CType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product Var CType -> [Symbol Var CType]
forall v c. Product v c -> [Symbol v c]
unP
  where
    go :: Symbol v c -> Maybe (SOP v c, Product v c)
go (E SOP v c
s1 Product v c
p1) = (SOP v c, Product v c) -> Maybe (SOP v c, Product v c)
forall a. a -> Maybe a
Just (SOP v c
s1,Product v c
p1)
    go Symbol v c
_         = Maybe (SOP v c, Product v c)
forall a. Maybe a
Nothing

-- | Find the 'TyVar' in a 'CoreSOP'
fvSOP :: CoreSOP -> UniqSet TyVar
fvSOP :: CoreSOP -> UniqSet Var
fvSOP = [UniqSet Var] -> UniqSet Var
forall a. [UniqSet a] -> UniqSet a
unionManyUniqSets ([UniqSet Var] -> UniqSet Var)
-> (CoreSOP -> [UniqSet Var]) -> CoreSOP -> UniqSet Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Product Var CType -> UniqSet Var)
-> [Product Var CType] -> [UniqSet Var]
forall a b. (a -> b) -> [a] -> [b]
map Product Var CType -> UniqSet Var
fvProduct ([Product Var CType] -> [UniqSet Var])
-> (CoreSOP -> [Product Var CType]) -> CoreSOP -> [UniqSet Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreSOP -> [Product Var CType]
forall v c. SOP v c -> [Product v c]
unS

fvProduct :: CoreProduct -> UniqSet TyVar
fvProduct :: Product Var CType -> UniqSet Var
fvProduct = [UniqSet Var] -> UniqSet Var
forall a. [UniqSet a] -> UniqSet a
unionManyUniqSets ([UniqSet Var] -> UniqSet Var)
-> (Product Var CType -> [UniqSet Var])
-> Product Var CType
-> UniqSet Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol Var CType -> UniqSet Var)
-> [Symbol Var CType] -> [UniqSet Var]
forall a b. (a -> b) -> [a] -> [b]
map Symbol Var CType -> UniqSet Var
fvSymbol ([Symbol Var CType] -> [UniqSet Var])
-> (Product Var CType -> [Symbol Var CType])
-> Product Var CType
-> [UniqSet Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product Var CType -> [Symbol Var CType]
forall v c. Product v c -> [Symbol v c]
unP

fvSymbol :: CoreSymbol -> UniqSet TyVar
fvSymbol :: Symbol Var CType -> UniqSet Var
fvSymbol (I Integer
_)   = UniqSet Var
forall a. UniqSet a
emptyUniqSet
fvSymbol (C CType
_)   = UniqSet Var
forall a. UniqSet a
emptyUniqSet
fvSymbol (V Var
v)   = Var -> UniqSet Var
forall a. Uniquable a => a -> UniqSet a
unitUniqSet Var
v
fvSymbol (E CoreSOP
s Product Var CType
p) = CoreSOP -> UniqSet Var
fvSOP CoreSOP
s UniqSet Var -> UniqSet Var -> UniqSet Var
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Product Var CType -> UniqSet Var
fvProduct Product Var CType
p

eqFV :: CoreSOP -> CoreSOP -> Bool
eqFV :: CoreSOP -> CoreSOP -> Bool
eqFV = UniqSet Var -> UniqSet Var -> Bool
forall a. Eq a => a -> a -> Bool
(==) (UniqSet Var -> UniqSet Var -> Bool)
-> (CoreSOP -> UniqSet Var) -> CoreSOP -> CoreSOP -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` CoreSOP -> UniqSet Var
fvSOP

containsConstants :: CoreSOP -> Bool
containsConstants :: CoreSOP -> Bool
containsConstants =
  (Product Var CType -> Bool) -> [Product Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Symbol Var CType -> Bool) -> [Symbol Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Symbol Var CType -> Bool
symbolContainsConstant ([Symbol Var CType] -> Bool)
-> (Product Var CType -> [Symbol Var CType])
-> Product Var CType
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product Var CType -> [Symbol Var CType]
forall v c. Product v c -> [Symbol v c]
unP) ([Product Var CType] -> Bool)
-> (CoreSOP -> [Product Var CType]) -> CoreSOP -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreSOP -> [Product Var CType]
forall v c. SOP v c -> [Product v c]
unS
  where
    symbolContainsConstant :: Symbol Var CType -> Bool
symbolContainsConstant Symbol Var CType
c = case Symbol Var CType
c of
      C {} -> Bool
True
      E CoreSOP
s Product Var CType
p -> CoreSOP -> Bool
containsConstants CoreSOP
s Bool -> Bool -> Bool
|| CoreSOP -> Bool
containsConstants ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
p])
      Symbol Var CType
_ -> Bool
False

safeDiv :: Integer -> Integer -> Maybe Integer
safeDiv :: Integer -> Integer -> Maybe Integer
safeDiv Integer
i Integer
j
  | Integer
j Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0    = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
  | Bool
otherwise = case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
j of
                  (Integer
k,Integer
0) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
k
                  (Integer, Integer)
_     -> Maybe Integer
forall a. Maybe a
Nothing

-- | Given `x` and `y`, return `Just n` when
--
-- `ceiling (logBase x y) == floor (logBase x y)`
integerLogBase :: Integer -> Integer -> Maybe Integer
integerLogBase :: Integer -> Integer -> Maybe Integer
integerLogBase Integer
x Integer
y | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
1 Bool -> Bool -> Bool
&& Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 =
  let z1 :: Int#
z1 = Integer -> Integer -> Int#
integerLogBase# Integer
x Integer
y
      z2 :: Int#
z2 = Integer -> Integer -> Int#
integerLogBase# Integer
x (Integer
yInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)
  in  if Int# -> Bool
isTrue# (Int#
z1 Int# -> Int# -> Int#
==# Int#
z2)
         then Maybe Integer
forall a. Maybe a
Nothing
         else Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Int# -> Integer
smallInteger Int#
z1)
integerLogBase Integer
_ Integer
_ = Maybe Integer
forall a. Maybe a
Nothing

isNatural :: CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural :: CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural (S [])           = Bool -> WriterT (Set CType) Maybe Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
isNatural (S [P []])       = Bool -> WriterT (Set CType) Maybe Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
isNatural (S [P (I Integer
i:[Symbol Var CType]
ps)])
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0    = CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
ps])
  | Bool
otherwise = Bool -> WriterT (Set CType) Maybe Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isNatural (S [P (V Var
_:[Symbol Var CType]
ps)]) = CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
ps])
isNatural (S [P (E CoreSOP
s Product Var CType
p:[Symbol Var CType]
ps)]) = do
  Bool
sN <- CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural CoreSOP
s
  Bool
pN <- CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
p])
  if Bool
sN Bool -> Bool -> Bool
&& Bool
pN
     then CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
ps])
     else Maybe (Bool, Set CType) -> WriterT (Set CType) Maybe Bool
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT Maybe (Bool, Set CType)
forall a. Maybe a
Nothing
-- This is a quick hack, it determines that
--
-- > a^b - 1
--
-- is a natural number as long as 'a' and 'b' are natural numbers.
-- This used to assert that:
--
-- > (1 <=? a^b) ~ True
isNatural (S [P [I (-1)],P [E CoreSOP
s Product Var CType
p]]) = Bool -> Bool -> Bool
(&&) (Bool -> Bool -> Bool)
-> WriterT (Set CType) Maybe Bool
-> WriterT (Set CType) Maybe (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural CoreSOP
s WriterT (Set CType) Maybe (Bool -> Bool)
-> WriterT (Set CType) Maybe Bool -> WriterT (Set CType) Maybe Bool
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
p])
-- We give up for all other products for now
isNatural (S [P (C CType
c:[Symbol Var CType]
ps)]) = do
  Set CType -> WriterT (Set CType) Maybe ()
forall (m :: * -> *) w. Monad m => w -> WriterT w m ()
tell (CType -> Set CType
forall a. a -> Set a
Set.singleton CType
c)
  CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
ps])
-- Adding two natural numbers is also a natural number
isNatural (S (Product Var CType
p:[Product Var CType]
ps)) = do
  Bool
pN <- CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
p])
  Bool
pK <- CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType]
ps)
  case (Bool
pN,Bool
pK) of
    (Bool
True,Bool
True)   -> Bool -> WriterT (Set CType) Maybe Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True  -- both are natural
    (Bool
False,Bool
False) -> Bool -> WriterT (Set CType) Maybe Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False -- both are non-natural
    (Bool, Bool)
_             -> Maybe (Bool, Set CType) -> WriterT (Set CType) Maybe Bool
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT Maybe (Bool, Set CType)
forall a. Maybe a
Nothing
    -- if one is natural and the other isn't, then their sum *might* be natural,
    -- but we simply cant be sure.

-- | Try to solve inequalities
solveIneq
  :: Word
  -- ^ Solving depth
  -> Ineq
  -- ^ Inequality we want to solve
  -> Ineq
  -- ^ Given/proven inequality
  -> WriterT (Set CType) Maybe Bool
  -- ^ Solver result
  --
  -- * /Nothing/: exhausted solver steps
  --
  -- * /Just True/: inequality is solved
  --
  -- * /Just False/: solver is unable to solve inequality, note that this does
  -- __not__ mean the wanted inequality does not hold.
solveIneq :: Word
-> (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT (Set CType) Maybe Bool
solveIneq Word
0 (CoreSOP, CoreSOP, Bool)
_ (CoreSOP, CoreSOP, Bool)
_ = WriterT (Set CType) Maybe Bool
forall a. WriterT (Set CType) Maybe a
noRewrite
solveIneq Word
k want :: (CoreSOP, CoreSOP, Bool)
want@(CoreSOP
_,CoreSOP
_,Bool
True) have :: (CoreSOP, CoreSOP, Bool)
have@(CoreSOP
_,CoreSOP
_,Bool
True)
  | (CoreSOP, CoreSOP, Bool)
want (CoreSOP, CoreSOP, Bool) -> (CoreSOP, CoreSOP, Bool) -> Bool
forall a. Eq a => a -> a -> Bool
== (CoreSOP, CoreSOP, Bool)
have
  = Bool -> WriterT (Set CType) Maybe Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  | Bool
otherwise
  = do
    let -- Apply all the rules, and get all the successful ones
        new :: [([((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))],
  Set CType)]
new     = (((CoreSOP, CoreSOP, Bool)
  -> (CoreSOP, CoreSOP, Bool)
  -> WriterT
       (Set CType)
       Maybe
       [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))])
 -> Maybe
      ([((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))],
       Set CType))
-> [(CoreSOP, CoreSOP, Bool)
    -> (CoreSOP, CoreSOP, Bool)
    -> WriterT
         (Set CType)
         Maybe
         [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]]
-> [([((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))],
     Set CType)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
f -> WriterT
  (Set CType)
  Maybe
  [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> Maybe
     ([((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))], Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT ((CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
f (CoreSOP, CoreSOP, Bool)
want (CoreSOP, CoreSOP, Bool)
have)) [(CoreSOP, CoreSOP, Bool)
 -> (CoreSOP, CoreSOP, Bool)
 -> WriterT
      (Set CType)
      Maybe
      [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]]
ineqRules
        -- Recurse down with all the transformed equations
        solved :: [([(Bool, Set CType)], Set CType)]
solved  = (([((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))],
  Set CType)
 -> ([(Bool, Set CType)], Set CType))
-> [([((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))],
     Set CType)]
-> [([(Bool, Set CType)], Set CType)]
forall a b. (a -> b) -> [a] -> [b]
map (([((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
 -> [(Bool, Set CType)])
-> ([((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))],
    Set CType)
-> ([(Bool, Set CType)], Set CType)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))
 -> Maybe (Bool, Set CType))
-> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> [(Bool, Set CType)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType))
-> (((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))
    -> WriterT (Set CType) Maybe Bool)
-> ((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))
-> Maybe (Bool, Set CType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((CoreSOP, CoreSOP, Bool)
 -> (CoreSOP, CoreSOP, Bool) -> WriterT (Set CType) Maybe Bool)
-> ((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))
-> WriterT (Set CType) Maybe Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Word
-> (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT (Set CType) Maybe Bool
solveIneq (Word
kWord -> Word -> Word
forall a. Num a => a -> a -> a
-Word
1))))) [([((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))],
  Set CType)]
new
        -- For the results of every recursive call, find the one that yields
        -- 'True' and has the smallest set of constraints.
        solved1 :: [((Bool, Set CType), Set CType)]
solved1 = (([(Bool, Set CType)], Set CType)
 -> ((Bool, Set CType), Set CType))
-> [([(Bool, Set CType)], Set CType)]
-> [((Bool, Set CType), Set CType)]
forall a b. (a -> b) -> [a] -> [b]
map (([(Bool, Set CType)] -> (Bool, Set CType))
-> ([(Bool, Set CType)], Set CType)
-> ((Bool, Set CType), Set CType)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first [(Bool, Set CType)] -> (Bool, Set CType)
forall a. [(Bool, Set a)] -> (Bool, Set a)
solvedInEqSmallestConstraint) [([(Bool, Set CType)], Set CType)]
solved
        -- Union the constraints from the corresponding rewrites with the
        -- constraints from the recursive results
        solved2 :: [(Bool, Set CType)]
solved2 = (((Bool, Set CType), Set CType) -> (Bool, Set CType))
-> [((Bool, Set CType), Set CType)] -> [(Bool, Set CType)]
forall a b. (a -> b) -> [a] -> [b]
map (\((Bool
b,Set CType
s1),Set CType
s2) -> (Bool
b,Set CType -> Set CType -> Set CType
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set CType
s1 Set CType
s2)) [((Bool, Set CType), Set CType)]
solved1
        -- From these results, again find the single result that yields 'True'
        -- and has the smallest set of constraints.
        solved3 :: (Bool, Set CType)
solved3 = [(Bool, Set CType)] -> (Bool, Set CType)
forall a. [(Bool, Set a)] -> (Bool, Set a)
solvedInEqSmallestConstraint [(Bool, Set CType)]
solved2
    if [([(Bool, Set CType)], Set CType)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([(Bool, Set CType)], Set CType)]
solved then
      WriterT (Set CType) Maybe Bool
forall a. WriterT (Set CType) Maybe a
noRewrite
    else do
      Maybe (Bool, Set CType) -> WriterT (Set CType) Maybe Bool
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT ((Bool, Set CType) -> Maybe (Bool, Set CType)
forall a. a -> Maybe a
Just (Bool, Set CType)
solved3)

solveIneq Word
_ (CoreSOP, CoreSOP, Bool)
_ (CoreSOP, CoreSOP, Bool)
_ = Bool -> WriterT (Set CType) Maybe Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

-- Find the solved inequality with the fewest number of constraints
solvedInEqSmallestConstraint :: [(Bool,Set a)] -> (Bool, Set a)
solvedInEqSmallestConstraint :: [(Bool, Set a)] -> (Bool, Set a)
solvedInEqSmallestConstraint = (Bool, Set a) -> [(Bool, Set a)] -> (Bool, Set a)
forall a. (Bool, Set a) -> [(Bool, Set a)] -> (Bool, Set a)
go (Bool
False, Set a
forall a. Set a
Set.empty)
 where
  go :: (Bool, Set a) -> [(Bool, Set a)] -> (Bool, Set a)
go (Bool, Set a)
bs [] = (Bool, Set a)
bs
  go (Bool
b,Set a
s) ((Bool
b1,Set a
s1):[(Bool, Set a)]
solved)
    | Bool -> Bool
not Bool
b Bool -> Bool -> Bool
&& Bool
b1
    = (Bool, Set a) -> [(Bool, Set a)] -> (Bool, Set a)
go (Bool
b1,Set a
s1) [(Bool, Set a)]
solved
    | Bool
b Bool -> Bool -> Bool
&& Bool
b1
    , Set a -> Int
forall a. Set a -> Int
Set.size Set a
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>  Set a -> Int
forall a. Set a -> Int
Set.size Set a
s1
    = (Bool, Set a) -> [(Bool, Set a)] -> (Bool, Set a)
go (Bool
b1,Set a
s1) [(Bool, Set a)]
solved
    | Bool
otherwise
    = (Bool, Set a) -> [(Bool, Set a)] -> (Bool, Set a)
go (Bool
b,Set a
s) [(Bool, Set a)]
solved

-- | Try to instantly solve an inequality by using the inequality solver using
-- @1 <=? 1 ~ True@ as the given constraint.
instantSolveIneq
  :: Word
  -- ^ Solving depth
  -> Ineq
  -- ^ Inequality we want to solve
  -> WriterT (Set CType) Maybe Bool
instantSolveIneq :: Word -> (CoreSOP, CoreSOP, Bool) -> WriterT (Set CType) Maybe Bool
instantSolveIneq Word
k (CoreSOP, CoreSOP, Bool)
u = Word
-> (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT (Set CType) Maybe Bool
solveIneq Word
k (CoreSOP, CoreSOP, Bool)
u (CoreSOP
forall v c. SOP v c
one,CoreSOP
forall v c. SOP v c
one,Bool
True)
 where
  one :: SOP v c
one = [Product v c] -> SOP v c
forall v c. [Product v c] -> SOP v c
S [[Symbol v c] -> Product v c
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol v c
forall v c. Integer -> Symbol v c
I Integer
1]]

type Ineq = (CoreSOP, CoreSOP, Bool)
type IneqRule = Ineq -> Ineq  -> WriterT (Set CType) Maybe [(Ineq,Ineq)]

noRewrite :: WriterT (Set CType) Maybe a
noRewrite :: WriterT (Set CType) Maybe a
noRewrite = Maybe (a, Set CType) -> WriterT (Set CType) Maybe a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT Maybe (a, Set CType)
forall a. Maybe a
Nothing

ineqRules
  :: [IneqRule]
ineqRules :: [(CoreSOP, CoreSOP, Bool)
 -> (CoreSOP, CoreSOP, Bool)
 -> WriterT
      (Set CType)
      Maybe
      [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]]
ineqRules =
  [ (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
leTrans
  , (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
plusMonotone
  , (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
timesMonotone
  , (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
powMonotone
  , (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
pow2MonotoneSpecial
  , (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
haveSmaller
  , (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
haveBigger
  ]

-- | Transitivity of inequality
leTrans :: IneqRule
leTrans :: (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
leTrans want :: (CoreSOP, CoreSOP, Bool)
want@(CoreSOP
a,CoreSOP
b,Bool
le) (CoreSOP
x,CoreSOP
y,Bool
_)
  -- want: 1 <=? y ~ True
  -- have: 2 <=? y ~ True
  --
  -- new want: want
  -- new have: 1 <=? y ~ True
  | S [P [I Integer
a']] <- CoreSOP
a
  , S [P [I Integer
x']] <- CoreSOP
x
  , Integer
x' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
a'
  = [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP, CoreSOP, Bool)
want,(CoreSOP
a,CoreSOP
y,Bool
le))]
  -- want: y <=? 10 ~ True
  -- have: y <=? 9 ~ True
  --
  -- new want: want
  -- new have: y <=? 10 ~ True
  | S [P [I Integer
b']] <- CoreSOP
b
  , S [P [I Integer
y']] <- CoreSOP
y
  , Integer
y' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
b'
  = [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP, CoreSOP, Bool)
want,(CoreSOP
x,CoreSOP
b,Bool
le))]
leTrans (CoreSOP, CoreSOP, Bool)
_ (CoreSOP, CoreSOP, Bool)
_ = WriterT
  (Set CType)
  Maybe
  [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall a. WriterT (Set CType) Maybe a
noRewrite

-- | Monotonicity of addition
--
-- We use SOP normalization to apply this rule by e.g.:
--
-- * Given: (2*x+1) <= (3*x-1)
-- * Turn to: (3*x-1) - (2*x+1)
-- * SOP version: -2 + x
-- * Convert back to inequality: 2 <= x
plusMonotone :: IneqRule
plusMonotone :: (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
plusMonotone (CoreSOP, CoreSOP, Bool)
want (CoreSOP, CoreSOP, Bool)
have
  | Just (CoreSOP, CoreSOP, Bool)
want' <- CoreSOP -> Maybe (CoreSOP, CoreSOP, Bool)
sopToIneq ((CoreSOP, CoreSOP, Bool) -> CoreSOP
subtractIneq (CoreSOP, CoreSOP, Bool)
want)
  , (CoreSOP, CoreSOP, Bool)
want' (CoreSOP, CoreSOP, Bool) -> (CoreSOP, CoreSOP, Bool) -> Bool
forall a. Eq a => a -> a -> Bool
/= (CoreSOP, CoreSOP, Bool)
want
  = [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP, CoreSOP, Bool)
want',(CoreSOP, CoreSOP, Bool)
have)]
  | Just (CoreSOP, CoreSOP, Bool)
have' <- CoreSOP -> Maybe (CoreSOP, CoreSOP, Bool)
sopToIneq ((CoreSOP, CoreSOP, Bool) -> CoreSOP
subtractIneq (CoreSOP, CoreSOP, Bool)
have)
  , (CoreSOP, CoreSOP, Bool)
have' (CoreSOP, CoreSOP, Bool) -> (CoreSOP, CoreSOP, Bool) -> Bool
forall a. Eq a => a -> a -> Bool
/= (CoreSOP, CoreSOP, Bool)
have
  = [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP, CoreSOP, Bool)
want,(CoreSOP, CoreSOP, Bool)
have')]
plusMonotone (CoreSOP, CoreSOP, Bool)
_ (CoreSOP, CoreSOP, Bool)
_ = WriterT
  (Set CType)
  Maybe
  [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall a. WriterT (Set CType) Maybe a
noRewrite

-- | Make the `a` of a given `a <= b` smaller
haveSmaller :: IneqRule
haveSmaller :: (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
haveSmaller (CoreSOP, CoreSOP, Bool)
want (CoreSOP, CoreSOP, Bool)
have
  | (S (Product Var CType
x:Product Var CType
y:[Product Var CType]
ys),CoreSOP
us,Bool
True) <- (CoreSOP, CoreSOP, Bool)
have
  = [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP, CoreSOP, Bool)
want,([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S (Product Var CType
xProduct Var CType -> [Product Var CType] -> [Product Var CType]
forall a. a -> [a] -> [a]
:[Product Var CType]
ys),CoreSOP
us,Bool
True))
    ,((CoreSOP, CoreSOP, Bool)
want,([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S (Product Var CType
yProduct Var CType -> [Product Var CType] -> [Product Var CType]
forall a. a -> [a] -> [a]
:[Product Var CType]
ys),CoreSOP
us,Bool
True))
    ]
  | (S [P [I Integer
1]], S [P (I Integer
_:p :: [Symbol Var CType]
p@(Symbol Var CType
_:[Symbol Var CType]
_))],Bool
True) <- (CoreSOP, CoreSOP, Bool)
have
  = [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP, CoreSOP, Bool)
want,([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
1]],[Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
p],Bool
True))]
haveSmaller (CoreSOP, CoreSOP, Bool)
_ (CoreSOP, CoreSOP, Bool)
_ = WriterT
  (Set CType)
  Maybe
  [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall a. WriterT (Set CType) Maybe a
noRewrite

-- | Make the `b` of a given `a <= b` bigger
haveBigger :: IneqRule
haveBigger :: (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
haveBigger (CoreSOP, CoreSOP, Bool)
want (CoreSOP, CoreSOP, Bool)
have
  | (CoreSOP
_ ,S [Product Var CType]
vs,Bool
True) <- (CoreSOP, CoreSOP, Bool)
want
  , (CoreSOP
as,S [Product Var CType]
bs,Bool
True) <- (CoreSOP, CoreSOP, Bool)
have
  , let vs' :: [Product Var CType]
vs' = [Product Var CType]
vs [Product Var CType] -> [Product Var CType] -> [Product Var CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Product Var CType]
bs
  , Bool -> Bool
not ([Product Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product Var CType]
vs')
  -- want : a <= x + 1
  -- have : y <= x
  --
  -- new want: want
  -- new have: y <= x + 1
  = do
    -- Ensure that we're actually making the RHS larger
    Bool
b <- CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType]
vs')
    if Bool
b then
      [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP, CoreSOP, Bool)
want,(CoreSOP
as,CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType]
bs) ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType]
vs'),Bool
True))]
    else
      WriterT
  (Set CType)
  Maybe
  [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall a. WriterT (Set CType) Maybe a
noRewrite
haveBigger (CoreSOP, CoreSOP, Bool)
_ (CoreSOP, CoreSOP, Bool)
_ = WriterT
  (Set CType)
  Maybe
  [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall a. WriterT (Set CType) Maybe a
noRewrite

-- | Monotonicity of multiplication
timesMonotone :: IneqRule
timesMonotone :: (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
timesMonotone want :: (CoreSOP, CoreSOP, Bool)
want@(CoreSOP
a,CoreSOP
b,Bool
le) have :: (CoreSOP, CoreSOP, Bool)
have@(CoreSOP
x,CoreSOP
y,Bool
_)
  -- want: C*a <=? b ~ True
  -- have: x <=? y ~ True
  --
  -- new want: want
  -- new have: C*a <=? C*y ~ True
  | S [P a' :: [Symbol Var CType]
a'@(Symbol Var CType
_:Symbol Var CType
_:[Symbol Var CType]
_)] <- CoreSOP
a
  , S [P [Symbol Var CType]
x'] <- CoreSOP
x
  , S [P [Symbol Var CType]
y'] <- CoreSOP
y
  , let ax :: [Symbol Var CType]
ax = [Symbol Var CType]
a' [Symbol Var CType] -> [Symbol Var CType] -> [Symbol Var CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol Var CType]
x'
  , let ay :: [Symbol Var CType]
ay = [Symbol Var CType]
a' [Symbol Var CType] -> [Symbol Var CType] -> [Symbol Var CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol Var CType]
y'
  -- Ensure we don't repeat this rule over and over
  , Bool -> Bool
not ([Symbol Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol Var CType]
ax)
  , Bool -> Bool
not ([Symbol Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol Var CType]
ay)
  -- Pick the smallest product
  , let az :: CoreSOP
az = if [Symbol Var CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol Var CType]
ax Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Symbol Var CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol Var CType]
ay then [Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
ax] else [Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
ay]
  = [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP, CoreSOP, Bool)
want,(CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul CoreSOP
az CoreSOP
x, CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul CoreSOP
az CoreSOP
y,Bool
le))]

  -- want: a <=? C*b ~ True
  -- have: x <=? y ~ True
  --
  -- new want: want
  -- new have: C*a <=? C*y ~ True
  | S [P b' :: [Symbol Var CType]
b'@(Symbol Var CType
_:Symbol Var CType
_:[Symbol Var CType]
_)] <- CoreSOP
b
  , S [P [Symbol Var CType]
x'] <- CoreSOP
x
  , S [P [Symbol Var CType]
y'] <- CoreSOP
y
  , let bx :: [Symbol Var CType]
bx = [Symbol Var CType]
b' [Symbol Var CType] -> [Symbol Var CType] -> [Symbol Var CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol Var CType]
x'
  , let by :: [Symbol Var CType]
by = [Symbol Var CType]
b' [Symbol Var CType] -> [Symbol Var CType] -> [Symbol Var CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol Var CType]
y'
  -- Ensure we don't repeat this rule over and over
  , Bool -> Bool
not ([Symbol Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol Var CType]
bx)
  , Bool -> Bool
not ([Symbol Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol Var CType]
by)
  -- Pick the smallest product
  , let bz :: CoreSOP
bz = if [Symbol Var CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol Var CType]
bx Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Symbol Var CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol Var CType]
by then [Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
bx] else [Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
by]
  = [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP, CoreSOP, Bool)
want,(CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul CoreSOP
bz CoreSOP
x, CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul CoreSOP
bz CoreSOP
y,Bool
le))]

  -- want: a <=? b ~ True
  -- have: C*x <=? y ~ True
  --
  -- new want: C*a <=? C*b ~ True
  -- new have: have
  | S [P x' :: [Symbol Var CType]
x'@(Symbol Var CType
_:Symbol Var CType
_:[Symbol Var CType]
_)] <- CoreSOP
x
  , S [P [Symbol Var CType]
a'] <- CoreSOP
a
  , S [P [Symbol Var CType]
b'] <- CoreSOP
b
  , let xa :: [Symbol Var CType]
xa = [Symbol Var CType]
x' [Symbol Var CType] -> [Symbol Var CType] -> [Symbol Var CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol Var CType]
a'
  , let xb :: [Symbol Var CType]
xb = [Symbol Var CType]
x' [Symbol Var CType] -> [Symbol Var CType] -> [Symbol Var CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol Var CType]
b'
  -- Ensure we don't repeat this rule over and over
  , Bool -> Bool
not ([Symbol Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol Var CType]
xa)
  , Bool -> Bool
not ([Symbol Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol Var CType]
xb)
  -- Pick the smallest product
  , let xz :: CoreSOP
xz = if [Symbol Var CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol Var CType]
xa Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Symbol Var CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol Var CType]
xb then [Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
xa] else [Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
xb]
  = [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul CoreSOP
xz CoreSOP
a, CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul CoreSOP
xz CoreSOP
b,Bool
le),(CoreSOP, CoreSOP, Bool)
have)]

  -- want: a <=? b ~ True
  -- have: x <=? C*y ~ True
  --
  -- new want: C*a <=? C*b ~ True
  -- new have: have
  | S [P y' :: [Symbol Var CType]
y'@(Symbol Var CType
_:Symbol Var CType
_:[Symbol Var CType]
_)] <- CoreSOP
y
  , S [P [Symbol Var CType]
a'] <- CoreSOP
a
  , S [P [Symbol Var CType]
b'] <- CoreSOP
b
  , let ya :: [Symbol Var CType]
ya = [Symbol Var CType]
y' [Symbol Var CType] -> [Symbol Var CType] -> [Symbol Var CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol Var CType]
a'
  , let yb :: [Symbol Var CType]
yb = [Symbol Var CType]
y' [Symbol Var CType] -> [Symbol Var CType] -> [Symbol Var CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol Var CType]
b'
  -- Ensure we don't repeat this rule over and over
  , Bool -> Bool
not ([Symbol Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol Var CType]
ya)
  , Bool -> Bool
not ([Symbol Var CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol Var CType]
yb)
  -- Pick the smallest product
  , let yz :: CoreSOP
yz = if [Symbol Var CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol Var CType]
ya Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Symbol Var CType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol Var CType]
yb then [Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
ya] else [Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Symbol Var CType]
yb]
  = [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul CoreSOP
yz CoreSOP
a, CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul CoreSOP
yz CoreSOP
b,Bool
le),(CoreSOP, CoreSOP, Bool)
have)]

timesMonotone (CoreSOP, CoreSOP, Bool)
_ (CoreSOP, CoreSOP, Bool)
_ = WriterT
  (Set CType)
  Maybe
  [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall a. WriterT (Set CType) Maybe a
noRewrite

-- | Monotonicity of exponentiation
powMonotone :: IneqRule
powMonotone :: (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
powMonotone (CoreSOP, CoreSOP, Bool)
want (CoreSOP
x, S [P [E CoreSOP
yS Product Var CType
yP]],Bool
le)
  = case CoreSOP
x of
      S [P [E CoreSOP
xS Product Var CType
xP]]
        -- want: XXX
        -- have: 2^x <=? 2^y ~ True
        --
        -- new want: want
        -- new have: x <=? y ~ True
        | CoreSOP
xS CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
== CoreSOP
yS
        -> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP, CoreSOP, Bool)
want,([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
xP],[Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
yP],Bool
le))]
        -- want: XXX
        -- have: x^2 <=? y^2 ~ True
        --
        -- new want: want
        -- new have: x <=? y ~ True
        | Product Var CType
xP Product Var CType -> Product Var CType -> Bool
forall a. Eq a => a -> a -> Bool
== Product Var CType
yP
        -> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP, CoreSOP, Bool)
want,(CoreSOP
xS,CoreSOP
yS,Bool
le))]
        -- want: XXX
        -- have: 2 <=? 2 ^ x ~ True
        --
        -- new want: want
        -- new have: 1 <=? x ~ True
      CoreSOP
_ | CoreSOP
x CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
== CoreSOP
yS
        -> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP, CoreSOP, Bool)
want,([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
1]],[Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
yP],Bool
le))]
      CoreSOP
_ -> WriterT
  (Set CType)
  Maybe
  [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall a. WriterT (Set CType) Maybe a
noRewrite

powMonotone (CoreSOP
a,S [P [E CoreSOP
bS Product Var CType
bP]],Bool
le) (CoreSOP, CoreSOP, Bool)
have
  = case CoreSOP
a of
      S [P [E CoreSOP
aS Product Var CType
aP]]
        -- want: 2^x <=? 2^y ~ True
        -- have: XXX
        --
        -- new want: x <=? y ~ True
        -- new have: have
        | CoreSOP
aS CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
== CoreSOP
bS
        -> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
aP],[Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
bP],Bool
le),(CoreSOP, CoreSOP, Bool)
have)]
        -- want: x^2 <=? y^2 ~ True
        -- have: XXX
        --
        -- new want: x <=? y ~ True
        -- new have: have
        | Product Var CType
aP Product Var CType -> Product Var CType -> Bool
forall a. Eq a => a -> a -> Bool
== Product Var CType
bP
        -> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP
aS,CoreSOP
bS,Bool
le),(CoreSOP, CoreSOP, Bool)
have)]
        -- want: 2 <=? 2 ^ x ~ True
        -- have: XXX
        --
        -- new want: 1 <=? x ~ True
        -- new have: XXX
      CoreSOP
_ | CoreSOP
a CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
== CoreSOP
bS
        -> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
1]],[Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
bP],Bool
le),(CoreSOP, CoreSOP, Bool)
have)]
      CoreSOP
_ -> WriterT
  (Set CType)
  Maybe
  [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall a. WriterT (Set CType) Maybe a
noRewrite

powMonotone (CoreSOP, CoreSOP, Bool)
_ (CoreSOP, CoreSOP, Bool)
_ = WriterT
  (Set CType)
  Maybe
  [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall a. WriterT (Set CType) Maybe a
noRewrite

-- | Try to get the power-of-2 factors, and apply the monotonicity of
-- exponentiation rule.
--
-- TODO: I wish we could generalize to find arbitrary factors, but currently
-- I don't know how.
pow2MonotoneSpecial :: IneqRule
pow2MonotoneSpecial :: (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
pow2MonotoneSpecial (CoreSOP
a,CoreSOP
b,Bool
le) (CoreSOP, CoreSOP, Bool)
have
  -- want: 4 * 4^x <=? 8^x ~ True
  -- have: XXX
  --
  -- want as pow 2 factors: 2^(2+2*x) <=? 2^(3*x) ~ True
  --
  -- new want: 2+2*x <=? 3*x ~ True
  -- new have: have
  | Just CoreSOP
a' <- Integer -> CoreSOP -> Maybe CoreSOP
facSOP Integer
2 CoreSOP
a
  , Just CoreSOP
b' <- Integer -> CoreSOP -> Maybe CoreSOP
facSOP Integer
2 CoreSOP
b
  = [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP
a',CoreSOP
b',Bool
le),(CoreSOP, CoreSOP, Bool)
have)]
pow2MonotoneSpecial (CoreSOP, CoreSOP, Bool)
want (CoreSOP
x,CoreSOP
y,Bool
le)
  -- want: XXX
  -- have:4 * 4^x <=? 8^x ~ True
  --
  -- have as pow 2 factors: 2^(2+2*x) <=? 2^(3*x) ~ True
  --
  -- new want: want
  -- new have: 2+2*x <=? 3*x ~ True
  | Just CoreSOP
x' <- Integer -> CoreSOP -> Maybe CoreSOP
facSOP Integer
2 CoreSOP
x
  , Just CoreSOP
y' <- Integer -> CoreSOP -> Maybe CoreSOP
facSOP Integer
2 CoreSOP
y
  = [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
-> WriterT
     (Set CType)
     Maybe
     [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((CoreSOP, CoreSOP, Bool)
want,(CoreSOP
x',CoreSOP
y',Bool
le))]
pow2MonotoneSpecial (CoreSOP, CoreSOP, Bool)
_ (CoreSOP, CoreSOP, Bool)
_ = WriterT
  (Set CType)
  Maybe
  [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall a. WriterT (Set CType) Maybe a
noRewrite

-- | Get the power of /N/ factors of a SOP term
facSOP
  :: Integer
  -- ^ The power /N/
  -> CoreSOP
  -> Maybe CoreSOP
facSOP :: Integer -> CoreSOP -> Maybe CoreSOP
facSOP Integer
n (S [P [Symbol Var CType]
ps]) = ([CoreSOP] -> CoreSOP) -> Maybe [CoreSOP] -> Maybe CoreSOP
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S ([Product Var CType] -> CoreSOP)
-> ([CoreSOP] -> [Product Var CType]) -> [CoreSOP] -> CoreSOP
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Product Var CType]] -> [Product Var CType]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Product Var CType]] -> [Product Var CType])
-> ([CoreSOP] -> [[Product Var CType]])
-> [CoreSOP]
-> [Product Var CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CoreSOP -> [Product Var CType])
-> [CoreSOP] -> [[Product Var CType]]
forall a b. (a -> b) -> [a] -> [b]
map CoreSOP -> [Product Var CType]
forall v c. SOP v c -> [Product v c]
unS) ((Symbol Var CType -> Maybe CoreSOP)
-> [Symbol Var CType] -> Maybe [CoreSOP]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Integer -> Symbol Var CType -> Maybe CoreSOP
facSymbol Integer
n) [Symbol Var CType]
ps)
facSOP Integer
_ CoreSOP
_          = Maybe CoreSOP
forall a. Maybe a
Nothing

-- | Get the power of /N/ factors of a Symbol
facSymbol
  :: Integer
  -- ^ The power
  -> CoreSymbol
  -> Maybe CoreSOP
facSymbol :: Integer -> Symbol Var CType -> Maybe CoreSOP
facSymbol Integer
n (I Integer
i)
  | Just Integer
j <- Integer -> Integer -> Maybe Integer
integerLogBase Integer
n Integer
i
  = CoreSOP -> Maybe CoreSOP
forall a. a -> Maybe a
Just ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [[Symbol Var CType] -> Product Var CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol Var CType
forall v c. Integer -> Symbol v c
I Integer
j]])
facSymbol Integer
n (E CoreSOP
s Product Var CType
p)
  | Just CoreSOP
s' <- Integer -> CoreSOP -> Maybe CoreSOP
facSOP Integer
n CoreSOP
s
  = CoreSOP -> Maybe CoreSOP
forall a. a -> Maybe a
Just (CoreSOP -> CoreSOP -> CoreSOP
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul CoreSOP
s' ([Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
p]))
facSymbol Integer
_ Symbol Var CType
_ = Maybe CoreSOP
forall a. Maybe a
Nothing