{-|
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
  , 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
    -- * Properties
  , isNatural
  )
where

-- External
import Control.Arrow (second)
import Control.Monad.Trans.Maybe
import Control.Monad.Trans.Writer.Strict
import Data.Function (on)
import Data.List     ((\\), intersect, mapAccumL, nub)
import Data.Maybe    (fromMaybe, mapMaybe)
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
import Outputable    (Outputable (..), (<+>), ($$), text)
import TcPluginM     (TcPluginM, tcPluginTrace)
import TcRnMonad     (Ct, ctEvidence, isGiven)
import TcRnTypes     (ctEvPred)
import TcTypeNats    (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,
                      typeNatSubTyCon, typeNatLeqTyCon)
import Type          (EqRel (NomEq), PredTree (EqPred), TyVar, classifyPredType,
                      coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy,
                      nonDetCmpType, PredType, mkPrimEqPred)
import TyCoRep       (Kind, Type (..), TyLit (..))
import TysWiredIn    (boolTy, promotedTrueDataCon)
import UniqSet       (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets,
                      unitUniqSet)

-- 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 ty1 :: Type
ty1) == :: CType -> CType -> Bool
== (CType ty2 :: Type
ty2) = Type -> Type -> Bool
eqType Type
ty1 Type
ty2

instance Ord CType where
  compare :: CType -> CType -> Ordering
compare (CType ty1 :: Type
ty1) (CType ty2 :: 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 ty :: Type
ty | Just ty1 :: Type
ty1 <- Type -> Maybe Type
coreView Type
ty = Type -> Writer [(Type, Type)] CoreSOP
normaliseNat Type
ty1
normaliseNat (TyVarTy v :: 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 i :: 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 tc :: TyCon
tc [x :: Type
x,y :: 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 (-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 t :: 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)]])

-- | 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 i :: Integer
i):ps :: [Symbol Var CType]
ps@(_:_))) | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== (-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 i :: Integer
i):ps :: [Symbol Var CType]
ps)) | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 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 ps :: 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 0
    combineP [p :: 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 (\p' :: Product Var CType
p' -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon
                                                [Integer -> Type
mkNumLitTy 0, Product Var CType -> Type
reifyProduct Product Var CType
p'])
                             Product Var CType -> Type
reifyProduct Either (Product Var CType) (Product Var CType)
p
    combineP [p1 :: Either (Product Var CType) (Product Var CType)
p1,p2 :: 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
      (\x :: 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
               (\y :: 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 0, Type
r])
               -- x neg, y pos
               (\y :: 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)
      (\x :: 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
               (\y :: 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
               (\y :: 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 (p :: Either (Product Var CType) (Product Var CType)
p:ps :: [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 (\x :: Product Var CType
x -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon
                                                    [Type
es, Product Var CType -> Type
reifyProduct Product Var CType
x])
                                  (\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 ps :: [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 (\t1 :: Type
t1 t2 :: 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 s :: CoreSOP
s p :: 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 s1 :: CoreSOP
s1 p1 :: Product Var CType
p1) (y :: Either (Symbol Var CType) (CoreSOP, [Product Var CType])
y:ys :: [Either (Symbol Var CType) (CoreSOP, [Product Var CType])]
ys)
      | Right (s2 :: CoreSOP
s2,p2 :: [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 x :: Symbol Var CType
x ys :: [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 i :: Integer
i)  )  = Integer -> Type
mkNumLitTy Integer
i
reifySymbol (Left (C c :: CType
c)  )  = CType -> Type
unCType CType
c
reifySymbol (Left (V v :: Var
v)  )  = Var -> Type
mkTyVarTy Var
v
reifySymbol (Left (E s :: CoreSOP
s p :: 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 (s1 :: CoreSOP
s1,s2 :: [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 (x :: CoreSOP
x,y :: CoreSOP
y,isLE :: 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 (-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 (-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 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 i :: Integer
i):l :: [Symbol Var CType]
l),r :: Product Var CType
r])
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 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 [r :: Product Var CType
r,P ((I i :: Integer
i:l :: [Symbol Var CType]
l))])
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 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 _ = 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 (x :: CoreSOP
x,S [P [V v :: Var
v]],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 _
  = Maybe CoreUnify
forall a. Maybe a
Nothing

subtractionToPred
  :: (Type,Type)
  -> (PredType, Kind)
subtractionToPred :: (Type, Type) -> (Type, Type)
subtractionToPred (x :: Type
x,y :: 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 -> SDoc
forall a. Outputable a => a -> SDoc
ppr v
siVar SDoc -> SDoc -> SDoc
<+> String -> SDoc
text " := " SDoc -> SDoc -> SDoc
<+> SOP v c -> SDoc
forall a. Outputable a => a -> SDoc
ppr SOP v c
siSOP
  ppr (UnifyItem {..}) = SOP v c -> SDoc
forall a. Outputable a => a -> SDoc
ppr SOP v c
siLHS SDoc -> SDoc -> SDoc
<+> String -> SDoc
text " :~ " 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 []                   u :: SOP v c
u = SOP v c
u
substsSOP ((SubstItem {..}):s :: [UnifyItem v c]
s) u :: 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 {}):s :: [UnifyItem v c]
s)   u :: 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 tv :: v
tv e :: 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 tv :: v
tv e :: 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 _  _ s :: Symbol v c
s@(I _) = [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 _  _ s :: Symbol v c
s@(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 tv :: v
tv e :: SOP v c
e (V tv' :: 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 tv :: v
tv e :: SOP v c
e (E s :: SOP v c
s p :: 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 s :: [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 {..}) = 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 {..}) = 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 Win          = String -> SDoc
text "Win"
  ppr (Draw subst :: [CoreUnify]
subst) = String -> SDoc
text "Draw" SDoc -> SDoc -> SDoc
<+> [CoreUnify] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [CoreUnify]
subst
  ppr Lose         = String -> SDoc
text "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
ct u :: CoreSOP
u v :: CoreSOP
v = do
  String -> SDoc -> TcPluginM ()
tcPluginTrace "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
ct u :: CoreSOP
u v :: 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 x :: CoreSOP
x y :: 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 _               = 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
ct u :: CoreSOP
u@(S [P [V x :: Var
x]]) v :: CoreSOP
v
  = case Type -> PredTree
classifyPredType (Type -> PredTree) -> Type -> PredTree
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 NomEq t1 :: Type
t1 _
        | 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]
      _ -> []
unifiers ct :: Ct
ct u :: CoreSOP
u v :: CoreSOP
v@(S [P [V x :: Var
x]])
  = case Type -> PredTree
classifyPredType (Type -> PredTree) -> Type -> PredTree
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 NomEq _ t2 :: 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]
      _ -> []
unifiers ct :: Ct
ct u :: CoreSOP
u@(S [P [C _]]) v :: CoreSOP
v
  = case Type -> PredTree
classifyPredType (Type -> PredTree) -> Type -> PredTree
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 NomEq t1 :: Type
t1 t2 :: 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]
      _ -> []
unifiers ct :: Ct
ct u :: CoreSOP
u v :: CoreSOP
v@(S [P [C _]])
  = case Type -> PredTree
classifyPredType (Type -> PredTree) -> Type -> PredTree
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 NomEq t1 :: Type
t1 t2 :: 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]
      _ -> []
unifiers ct :: Ct
ct u :: CoreSOP
u v :: 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
_ct (S [P [V x :: 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 0]])]
unifiers' _ct :: Ct
_ct (S [])        (S [P [V x :: 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 0]])]

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

unifiers' _ct :: Ct
_ct s1 :: CoreSOP
s1@(S [P [C _]]) s2 :: 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
_ct s1 :: CoreSOP
s1               s2 :: CoreSOP
s2@(S [P [C _]]) = [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
ct (S [P [E s1 :: CoreSOP
s1 p1 :: Product Var CType
p1]]) (S [P [E s2 :: CoreSOP
s2 p2 :: 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
ct (S [P [E (S [P s1 :: [Symbol Var CType]
s1]) p1 :: Product Var CType
p1]]) (S [P p2 :: [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 (-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
ct (S [P p2 :: [Symbol Var CType]
p2]) (S [P [E (S [P s1 :: [Symbol Var CType]
s1]) p1 :: 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 (-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
ct (S [P [E (S [P [I i :: Integer
i]]) p :: Product Var CType
p]]) (S [P [I j :: Integer
j]])
  = case Integer -> Integer -> Maybe Integer
integerLogBase Integer
i Integer
j of
      Just k :: 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]])
      Nothing -> []

unifiers' ct :: Ct
ct (S [P [I j :: Integer
j]]) (S [P [E (S [P [I i :: Integer
i]]) p :: Product Var CType
p]])
  = case Integer -> Integer -> Maybe Integer
integerLogBase Integer
i Integer
j of
      Just k :: 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]])
      Nothing -> []

-- a^d * a^e ~ a^c ==> [c := d + e]
unifiers' ct :: Ct
ct (S [P [E s1 :: CoreSOP
s1 p1 :: Product Var CType
p1]]) (S [p2 :: Product Var CType
p2]) = case Product Var CType -> Maybe ([CoreSOP], [Product Var CType])
collectBases Product Var CType
p2 of
  Just (b :: CoreSOP
b:bs :: [CoreSOP]
bs,ps :: [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)
  _ -> []

unifiers' ct :: Ct
ct (S [p2 :: Product Var CType
p2]) (S [P [E s1 :: CoreSOP
s1 p1 :: Product Var CType
p1]]) = case Product Var CType -> Maybe ([CoreSOP], [Product Var CType])
collectBases Product Var CType
p2 of
  Just (b :: CoreSOP
b:bs :: [CoreSOP]
bs,ps :: [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])
  _ -> []

-- (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
ct (S [P ((I i :: Integer
i):ps :: [Symbol Var CType]
ps)]) (S [P [I j :: Integer
j]]) =
  case Integer -> Integer -> Maybe Integer
safeDiv Integer
j Integer
i of
    Just k :: 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]])
    _       -> []

unifiers' ct :: Ct
ct (S [P [I j :: Integer
j]]) (S [P ((I i :: Integer
i):ps :: [Symbol Var CType]
ps)]) =
  case Integer -> Integer -> Maybe Integer
safeDiv Integer
j Integer
i of
    Just k :: 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]])
    _       -> []

-- (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
ct (S [P ps1 :: [Symbol Var CType]
ps1]) (S [P ps2 :: [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 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 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
ct (S ((P [I i :: Integer
i]):ps1 :: [Product Var CType]
ps1)) (S ((P [I j :: Integer
j]):ps2 :: [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
ct s1 :: CoreSOP
s1@(S ps1 :: [Product Var CType]
ps1) s2 :: CoreSOP
s2@(S ps2 :: [Product Var CType]
ps2) = case CoreSOP -> Maybe (CoreSOP, CoreSOP, Bool)
sopToIneq CoreSOP
k1 of
  Just (s1' :: CoreSOP
s1',s2' :: CoreSOP
s2',_)
    | 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'
  _ | [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 (\x :: Product Var CType
x y :: 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)
        [k :: 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]
        _   -> []
    | [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
    -> []
  _ -> 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 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 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
ct (S [P [I i :: Integer
i],P [V v :: Var
v]]) s2 :: 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
ct s1 :: CoreSOP
s1 (S [P [I i :: Integer
i],P [V 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'' _ _ _ = []

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 s1 :: SOP v c
s1 p1 :: 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 _         = 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 _)   = UniqSet Var
forall a. UniqSet a
emptyUniqSet
fvSymbol (C _)   = UniqSet Var
forall a. UniqSet a
emptyUniqSet
fvSymbol (V v :: Var
v)   = Var -> UniqSet Var
forall a. Uniquable a => a -> UniqSet a
unitUniqSet Var
v
fvSymbol (E s :: CoreSOP
s p :: 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 (\c :: Symbol Var CType
c -> case Symbol Var CType
c of {(C _) -> Bool
True; _ -> Bool
False}) ([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

safeDiv :: Integer -> Integer -> Maybe Integer
safeDiv :: Integer -> Integer -> Maybe Integer
safeDiv i :: Integer
i j :: Integer
j
  | Integer
j Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0    = Integer -> Maybe Integer
forall a. a -> Maybe a
Just 0
  | Bool
otherwise = case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
j of
                  (k :: Integer
k,0) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
k
                  _     -> 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 x :: Integer
x y :: Integer
y | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> 1 Bool -> Bool -> Bool
&& Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> 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
-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 _ _ = 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 i :: Integer
i:ps :: [Symbol Var CType]
ps)])
  | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= 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 _:ps :: [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 s :: CoreSOP
s p :: Product Var CType
p:ps :: [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 s :: CoreSOP
s p :: 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 c :: CType
c:ps :: [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 (p :: Product Var CType
p:ps :: [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
    (True,True)   -> Bool -> WriterT (Set CType) Maybe Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True  -- both are natural
    (False,False) -> Bool -> WriterT (Set CType) Maybe Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False -- both are non-natural
    _             -> 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
  -> 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)
-> Maybe Bool
solveIneq 0 _ _ = Maybe Bool
forall a. Maybe a
Nothing
solveIneq k :: Word
k want :: (CoreSOP, CoreSOP, Bool)
want@(_,_,True) have :: (CoreSOP, CoreSOP, Bool)
have@(_,_,True)
  | (CoreSOP, CoreSOP, Bool)
want (CoreSOP, CoreSOP, Bool) -> (CoreSOP, CoreSOP, Bool) -> Bool
forall a. Eq a => a -> a -> Bool
== (CoreSOP, CoreSOP, Bool)
have
  = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
  | [Bool] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Bool]
solved
  = Maybe Bool
forall a. Maybe a
Nothing
  | Bool
otherwise
  = Bool -> Maybe Bool
forall a. a -> Maybe a
Just ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
solved)
  where
    solved :: [Bool]
solved = (((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))
 -> Maybe Bool)
-> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))] -> [Bool]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (((CoreSOP, CoreSOP, Bool)
 -> (CoreSOP, CoreSOP, Bool) -> Maybe Bool)
-> ((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))
-> Maybe Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Word
-> (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> Maybe Bool
solveIneq (Word
k Word -> Word -> Word
forall a. Num a => a -> a -> a
- 1))) [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
new
    new :: [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
new    = (((CoreSOP, CoreSOP, Bool)
  -> (CoreSOP, CoreSOP, Bool)
  -> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))])
 -> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))])
-> [(CoreSOP, CoreSOP, Bool)
    -> (CoreSOP, CoreSOP, Bool)
    -> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]]
-> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\f :: (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
f -> (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
f (CoreSOP, CoreSOP, Bool)
want (CoreSOP, CoreSOP, Bool)
have) [(CoreSOP, CoreSOP, Bool)
 -> (CoreSOP, CoreSOP, Bool)
 -> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]]
ineqRules
solveIneq _ _ _ = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False

-- | 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
  -> Bool
instantSolveIneq :: Word -> (CoreSOP, CoreSOP, Bool) -> Bool
instantSolveIneq k :: Word
k u :: (CoreSOP, CoreSOP, Bool)
u = case Word
-> (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> 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) of
  Just p :: Bool
p  -> Bool
p
  Nothing -> Bool
False
 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 1]]

type Ineq = (CoreSOP, CoreSOP, Bool)
type IneqRule = Ineq -> Ineq  -> [(Ineq,Ineq)]

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

-- | Transitivity of inequality
leTrans :: IneqRule
leTrans :: (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
leTrans want :: (CoreSOP, CoreSOP, Bool)
want@(a :: CoreSOP
a,b :: CoreSOP
b,le :: Bool
le) (x :: CoreSOP
x,y :: CoreSOP
y,_)
  -- want: 1 <=? y ~ True
  -- have: 2 <=? y ~ True
  --
  -- new want: want
  -- new have: 1 <=? y ~ True
  | S [P [I a' :: Integer
a']] <- CoreSOP
a
  , S [P [I x' :: Integer
x']] <- CoreSOP
x
  , Integer
x' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
a'
  = [((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 b' :: Integer
b']] <- CoreSOP
b
  , S [P [I y' :: Integer
y']] <- CoreSOP
y
  , Integer
y' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
b'
  = [((CoreSOP, CoreSOP, Bool)
want,(CoreSOP
x,CoreSOP
b,Bool
le))]
leTrans _ _ = []

-- | 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)
-> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
plusMonotone want :: (CoreSOP, CoreSOP, Bool)
want have :: (CoreSOP, CoreSOP, Bool)
have
  | Just want' :: (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)
want',(CoreSOP, CoreSOP, Bool)
have)]
  | Just have' :: (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)
want,(CoreSOP, CoreSOP, Bool)
have')]
plusMonotone _ _ = []

-- | Make the `a` of a given `a <= b` smaller
haveSmaller :: IneqRule
haveSmaller :: (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
haveSmaller want :: (CoreSOP, CoreSOP, Bool)
want have :: (CoreSOP, CoreSOP, Bool)
have
  | (S (x :: Product Var CType
x:y :: Product Var CType
y:ys :: [Product Var CType]
ys),us :: CoreSOP
us,True) <- (CoreSOP, CoreSOP, Bool)
have
  = [((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 1]], S [P (I _:p :: [Symbol Var CType]
p@(_:_))],True) <- (CoreSOP, CoreSOP, Bool)
have
  = [((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 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 _ _ = []

-- | Make the `b` of a given `a <= b` bigger
haveBigger :: IneqRule
haveBigger :: (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
haveBigger want :: (CoreSOP, CoreSOP, Bool)
want have :: (CoreSOP, CoreSOP, Bool)
have
  | (_,S vs :: [Product Var CType]
vs,True) <- (CoreSOP, CoreSOP, Bool)
want
  , (as :: CoreSOP
as,S bs :: [Product Var CType]
bs,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
  = [((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))]
haveBigger _ _ = []

-- | Monotonicity of multiplication
timesMonotone :: IneqRule
timesMonotone :: (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
timesMonotone want :: (CoreSOP, CoreSOP, Bool)
want@(a :: CoreSOP
a,b :: CoreSOP
b,le :: Bool
le) have :: (CoreSOP, CoreSOP, Bool)
have@(x :: CoreSOP
x,y :: CoreSOP
y,_)
  -- 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'@(_:_:_)] <- CoreSOP
a
  , S [P x' :: [Symbol Var CType]
x'] <- CoreSOP
x
  , S [P y' :: [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)
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'@(_:_:_)] <- CoreSOP
b
  , S [P x' :: [Symbol Var CType]
x'] <- CoreSOP
x
  , S [P y' :: [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)
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'@(_:_:_)] <- CoreSOP
x
  , S [P a' :: [Symbol Var CType]
a'] <- CoreSOP
a
  , S [P b' :: [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 -> 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'@(_:_:_)] <- CoreSOP
y
  , S [P a' :: [Symbol Var CType]
a'] <- CoreSOP
a
  , S [P b' :: [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 -> 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 _ _ = []

-- | Monotonicity of exponentiation
powMonotone :: IneqRule
powMonotone :: (CoreSOP, CoreSOP, Bool)
-> (CoreSOP, CoreSOP, Bool)
-> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
powMonotone want :: (CoreSOP, CoreSOP, Bool)
want (x :: CoreSOP
x, S [P [E yS :: CoreSOP
yS yP :: Product Var CType
yP]],le :: Bool
le)
  = case CoreSOP
x of
      S [P [E xS :: CoreSOP
xS xP :: 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)
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)
want,(CoreSOP
xS,CoreSOP
yS,Bool
le))]
        -- want: XXX
        -- have: 2 <=? 2 ^ x ~ True
        --
        -- new want: want
        -- new have: 1 <=? x ~ True
      _ | CoreSOP
x CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
== CoreSOP
yS
        -> [((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 1]],[Product Var CType] -> CoreSOP
forall v c. [Product v c] -> SOP v c
S [Product Var CType
yP],Bool
le))]
      _ -> []

powMonotone (a :: CoreSOP
a,S [P [E bS :: CoreSOP
bS bP :: Product Var CType
bP]],le :: Bool
le) have :: (CoreSOP, CoreSOP, Bool)
have
  = case CoreSOP
a of
      S [P [E aS :: CoreSOP
aS aP :: 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
        -> [(([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
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
a CoreSOP -> CoreSOP -> Bool
forall a. Eq a => a -> a -> Bool
== CoreSOP
bS
        -> [(([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 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)]
      _ -> []

powMonotone _ _ = []

-- | 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)
-> [((CoreSOP, CoreSOP, Bool), (CoreSOP, CoreSOP, Bool))]
pow2MonotoneSpecial (a :: CoreSOP
a,b :: CoreSOP
b,le :: Bool
le) have :: (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 a' :: CoreSOP
a' <- Integer -> CoreSOP -> Maybe CoreSOP
facSOP 2 CoreSOP
a
  , Just b' :: CoreSOP
b' <- Integer -> CoreSOP -> Maybe CoreSOP
facSOP 2 CoreSOP
b
  = [((CoreSOP
a',CoreSOP
b',Bool
le),(CoreSOP, CoreSOP, Bool)
have)]
pow2MonotoneSpecial want :: (CoreSOP, CoreSOP, Bool)
want (x :: CoreSOP
x,y :: CoreSOP
y,le :: 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 x' :: CoreSOP
x' <- Integer -> CoreSOP -> Maybe CoreSOP
facSOP 2 CoreSOP
x
  , Just y' :: CoreSOP
y' <- Integer -> CoreSOP -> Maybe CoreSOP
facSOP 2 CoreSOP
y
  = [((CoreSOP, CoreSOP, Bool)
want,(CoreSOP
x',CoreSOP
y',Bool
le))]
pow2MonotoneSpecial _ _ = []

-- | Get the power of /N/ factors of a SOP term
facSOP
  :: Integer
  -- ^ The power /N/
  -> CoreSOP
  -> Maybe CoreSOP
facSOP :: Integer -> CoreSOP -> Maybe CoreSOP
facSOP n :: Integer
n (S [P ps :: [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 _ _          = 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 n :: Integer
n (I i :: Integer
i)
  | Just j :: 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 n :: Integer
n (E s :: CoreSOP
s p :: Product Var CType
p)
  | Just s' :: 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 _ _ = Maybe CoreSOP
forall a. Maybe a
Nothing