-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | GHC typechecker plugin for types of kind GHC.TypeLits.Nat
--   
--   A type checker plugin for GHC that can solve <i>equalities</i> and
--   <i>inequalities</i> of types of kind <tt>Nat</tt>, where these types
--   are either:
--   
--   <ul>
--   <li>Type-level naturals</li>
--   <li>Type variables</li>
--   <li>Applications of the arithmetic expressions
--   <tt>(+,-,*,^)</tt>.</li>
--   </ul>
--   
--   It solves these equalities by normalising them to <i>sort-of</i>
--   <tt>SOP</tt> (Sum-of-Products) form, and then perform a simple
--   syntactic equality.
--   
--   For example, this solver can prove the equality between:
--   
--   <pre>
--   (x + 2)^(y + 2)
--   </pre>
--   
--   and
--   
--   <pre>
--   4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2
--   </pre>
--   
--   Because the latter is actually the <tt>SOP</tt> normal form of the
--   former.
--   
--   To use the plugin, add the
--   
--   <pre>
--   OPTIONS_GHC -fplugin GHC.TypeLits.Normalise
--   </pre>
--   
--   Pragma to the header of your file.
@package ghc-typelits-natnormalise
@version 0.7.9


-- | <h1>SOP: Sum-of-Products, sorta</h1>
--   
--   The arithmetic operation for <a>Nat</a> are, addition
--   (<tt><a>+</a></tt>), subtraction (<tt><a>-</a></tt>), multiplication
--   (<tt><a>*</a></tt>), and exponentiation (<tt><a>^</a></tt>). This
--   means we cannot write expressions in a canonical SOP normal form. We
--   can get rid of subtraction by working with integers, and translating
--   <tt>a - b</tt> to <tt>a + (-1)*b</tt>. Exponentation cannot be getten
--   rid of that way. So we define the following grammar for our canonical
--   SOP-like normal form of arithmetic expressions:
--   
--   <pre>
--   SOP      ::= Product '+' SOP | Product
--   Product  ::= Symbol '*' Product | Symbol
--   Symbol   ::= Integer
--             |  Var
--             |  Var '^' Product
--             |  SOP '^' ProductE
--   
--   ProductE ::= SymbolE '*' ProductE | SymbolE
--   SymbolE  ::= Var
--             |  Var '^' Product
--             |  SOP '^' ProductE
--   </pre>
--   
--   So a valid SOP terms are:
--   
--   <pre>
--   x*y + y^2
--   (x+y)^(k*z)
--   </pre>
--   
--   , but,
--   
--   <pre>
--   (x*y)^2
--   </pre>
--   
--   is not, and should be:
--   
--   <pre>
--   x^2 * y^2
--   </pre>
--   
--   Exponents are thus not allowed to have products, so for example, the
--   expression:
--   
--   <pre>
--   (x + 2)^(y + 2)
--   </pre>
--   
--   in valid SOP form is:
--   
--   <pre>
--   4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2
--   </pre>
--   
--   Also, exponents can only be integer values when the base is a
--   variable. Although not enforced by the grammar, the exponentials are
--   flatted as far as possible in SOP form. So:
--   
--   <pre>
--   (x^y)^z
--   </pre>
--   
--   is flattened to:
--   
--   <pre>
--   x^(y*z)
--   </pre>
module GHC.TypeLits.Normalise.SOP
data Symbol v c

-- | Integer constant
I :: Integer -> Symbol v c

-- | Non-integer constant
C :: c -> Symbol v c

-- | Exponentiation
E :: SOP v c -> Product v c -> Symbol v c

-- | Variable
V :: v -> Symbol v c
newtype Product v c
P :: [Symbol v c] -> Product v c
[unP] :: Product v c -> [Symbol v c]
newtype SOP v c
S :: [Product v c] -> SOP v c
[unS] :: SOP v c -> [Product v c]

-- | reduce exponentials
--   
--   Performs the following rewrites:
--   
--   <pre>
--   x^0          ==&gt;  1
--   0^x          ==&gt;  0
--   2^3          ==&gt;  8
--   (k ^ i) ^ j  ==&gt;  k ^ (i * j)
--   </pre>
reduceExp :: (Ord v, Ord c) => Symbol v c -> Symbol v c

-- | Merge two symbols of a Product term
--   
--   Performs the following rewrites:
--   
--   <pre>
--   8 * 7    ==&gt;  56
--   1 * x    ==&gt;  x
--   x * 1    ==&gt;  x
--   0 * x    ==&gt;  0
--   x * 0    ==&gt;  0
--   x * x^4  ==&gt;  x^5
--   x^4 * x  ==&gt;  x^5
--   y*y      ==&gt;  y^2
--   </pre>
mergeS :: (Ord v, Ord c) => Symbol v c -> Symbol v c -> Either (Symbol v c) (Symbol v c)

-- | Merge two products of a SOP term
--   
--   Performs the following rewrites:
--   
--   <pre>
--   2xy + 3xy  ==&gt;  5xy
--   2xy + xy   ==&gt;  3xy
--   xy + 2xy   ==&gt;  3xy
--   xy + xy    ==&gt;  2xy
--   </pre>
mergeP :: (Eq v, Eq c) => Product v c -> Product v c -> Either (Product v c) (Product v c)

-- | Merge two SOP terms by additions
mergeSOPAdd :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c

-- | Merge two SOP terms by multiplication
mergeSOPMul :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c

-- | Expand or Simplify <tt>complex</tt> exponentials
--   
--   Performs the following rewrites:
--   
--   <pre>
--   b^1              ==&gt;  b
--   2^(y^2)          ==&gt;  4^y
--   (x + 2)^2        ==&gt;  x^2 + 4xy + 4
--   (x + 2)^(2x)     ==&gt;  (x^2 + 4xy + 4)^x
--   (x + 2)^(y + 2)  ==&gt;  4x(2 + x)^y + 4(2 + x)^y + (2 + x)^yx^2
--   </pre>
normaliseExp :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c

-- | Simplifies SOP terms using
--   
--   <ul>
--   <li><a>mergeS</a></li>
--   <li><a>mergeP</a></li>
--   <li><a>reduceExp</a></li>
--   </ul>
simplifySOP :: (Ord v, Ord c) => SOP v c -> SOP v c
instance (GHC.Classes.Ord c, GHC.Classes.Ord v) => GHC.Classes.Ord (GHC.TypeLits.Normalise.SOP.Symbol v c)
instance (GHC.Classes.Eq c, GHC.Classes.Eq v) => GHC.Classes.Eq (GHC.TypeLits.Normalise.SOP.Symbol v c)
instance (GHC.Classes.Eq c, GHC.Classes.Eq v) => GHC.Classes.Eq (GHC.TypeLits.Normalise.SOP.Product v c)
instance (GHC.Classes.Ord v, GHC.Classes.Ord c) => GHC.Classes.Ord (GHC.TypeLits.Normalise.SOP.SOP v c)
instance (GHC.Classes.Ord v, GHC.Classes.Ord c) => GHC.Classes.Ord (GHC.TypeLits.Normalise.SOP.Product v c)
instance (GHC.Classes.Eq v, GHC.Classes.Eq c) => GHC.Classes.Eq (GHC.TypeLits.Normalise.SOP.SOP v c)
instance (GHC.Utils.Outputable.Outputable v, GHC.Utils.Outputable.Outputable c) => GHC.Utils.Outputable.Outputable (GHC.TypeLits.Normalise.SOP.SOP v c)
instance (GHC.Utils.Outputable.Outputable v, GHC.Utils.Outputable.Outputable c) => GHC.Utils.Outputable.Outputable (GHC.TypeLits.Normalise.SOP.Product v c)
instance (GHC.Utils.Outputable.Outputable v, GHC.Utils.Outputable.Outputable c) => GHC.Utils.Outputable.Outputable (GHC.TypeLits.Normalise.SOP.Symbol v c)


module GHC.TypeLits.Normalise.Unify
newtype CType
CType :: Type -> CType
[unCType] :: CType -> Type

-- | <a>SOP</a> with <a>TyVar</a> variables
type CoreSOP = SOP TyVar CType

-- | Convert a type of <i>kind</i> <a>Nat</a> to an <a>SOP</a> term, but
--   only when the type is constructed out of:
--   
--   <ul>
--   <li>literals</li>
--   <li>type variables</li>
--   <li>Applications of the arithmetic operators <tt>(+,-,*,^)</tt></li>
--   </ul>
normaliseNat :: Type -> Writer [(Type, Type)] CoreSOP

-- | Applies <a>normaliseNat</a> and <a>simplifySOP</a> to type or
--   predicates to reduce any occurrences of sub-terms of <i>kind</i>
--   <a>Nat</a>. If the result is the same as input, returns
--   <tt><a>Nothing</a></tt>.
normaliseNatEverywhere :: Type -> Writer [(Type, Type)] (Maybe Type)
normaliseSimplifyNat :: Type -> Writer [(Type, Type)] Type

-- | Convert a <a>SOP</a> term back to a type of <i>kind</i> <a>Nat</a>
reifySOP :: CoreSOP -> Type
data UnifyItem v c
SubstItem :: v -> SOP v c -> UnifyItem v c
[siVar] :: UnifyItem v c -> v
[siSOP] :: UnifyItem v c -> SOP v c
UnifyItem :: SOP v c -> SOP v c -> UnifyItem v c
[siLHS] :: UnifyItem v c -> SOP v c
[siRHS] :: UnifyItem v c -> SOP v c

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

-- | Apply a substitution to a single normalised <a>SOP</a> term
substsSOP :: (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c

-- | Apply a substitution to a substitution
substsSubst :: (Ord v, Ord c) => [UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c]

-- | Result of comparing two <a>SOP</a> terms, returning a potential
--   substitution list under which the two terms are equal.
data UnifyResult

-- | Two terms are equal
Win :: UnifyResult

-- | Two terms are <i>not</i> equal
Lose :: UnifyResult

-- | Two terms are only equal if the given substitution holds
Draw :: [CoreUnify] -> UnifyResult

-- | Given two <a>SOP</a>s <tt>u</tt> and <tt>v</tt>, when their free
--   variables (<a>fvSOP</a>) are the same, then we <a>Win</a> if
--   <tt>u</tt> and <tt>v</tt> are equal, and <a>Lose</a> otherwise.
--   
--   If <tt>u</tt> and <tt>v</tt> do not have the same free variables, we
--   result in a <a>Draw</a>, ware <tt>u</tt> and <tt>v</tt> are only equal
--   when the returned <tt>CoreSubst</tt> holds.
unifyNats :: Ct -> CoreSOP -> CoreSOP -> TcPluginM UnifyResult

-- | Find unifiers for two SOP terms
--   
--   Can find the following unifiers:
--   
--   <pre>
--   t ~ a + b          ==&gt;  [t := a + b]
--   a + b ~ t          ==&gt;  [t := a + b]
--   (a + c) ~ (b + c)  ==&gt;  &lt;math&gt;
--   (2*a) ~ (2*b)      ==&gt;  [a := b]
--   (2 + a) ~ 5        ==&gt;  [a := 3]
--   (i * a) ~ j        ==&gt;  [a := div j i], when (mod j i == 0)
--   </pre>
--   
--   However, given a wanted:
--   
--   <pre>
--   [W] t ~ a + b
--   </pre>
--   
--   this function returns <tt>[]</tt>, or otherwise we "solve" the
--   constraint by finding a unifier equal to the constraint.
--   
--   However, given a wanted:
--   
--   <pre>
--   [W] (a + c) ~ (b + c)
--   </pre>
--   
--   we do return the unifier:
--   
--   <pre>
--   [a := b]
--   </pre>
unifiers :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]

-- | Find the <a>TyVar</a> in a <a>CoreSOP</a>
fvSOP :: CoreSOP -> UniqSet TyVar

-- | Subtract an inequality, in order to either:
--   
--   <ul>
--   <li>See if the smallest solution is a natural number</li>
--   <li>Cancel sums, i.e. monotonicity of addition</li>
--   </ul>
--   
--   <pre>
--   subtractIneq (2*y &lt;=? 3*x ~ True)  = (-2*y + 3*x)
--   subtractIneq (2*y &lt;=? 3*x ~ False) = (-3*x + (-1) + 2*y)
--   </pre>
subtractIneq :: (CoreSOP, CoreSOP, Bool) -> CoreSOP

-- | Try to solve inequalities
solveIneq :: Word -> Ineq -> Ineq -> WriterT (Set CType) Maybe Bool

-- | Give the smallest solution for an inequality
ineqToSubst :: Ineq -> Maybe CoreUnify
subtractionToPred :: TyCon -> (Type, Type) -> (PredType, Kind)

-- | Try to instantly solve an inequality by using the inequality solver
--   using <tt>1 &lt;=? 1 ~ True</tt> as the given constraint.
instantSolveIneq :: Word -> Ineq -> WriterT (Set CType) Maybe Bool
solvedInEqSmallestConstraint :: [(Bool, Set a)] -> (Bool, Set a)
isNatural :: CoreSOP -> WriterT (Set CType) Maybe Bool
instance GHC.Utils.Outputable.Outputable GHC.TypeLits.Normalise.Unify.CType
instance (GHC.Classes.Eq v, GHC.Classes.Eq c) => GHC.Classes.Eq (GHC.TypeLits.Normalise.Unify.UnifyItem v c)
instance GHC.Utils.Outputable.Outputable GHC.TypeLits.Normalise.Unify.UnifyResult
instance (GHC.Utils.Outputable.Outputable v, GHC.Utils.Outputable.Outputable c) => GHC.Utils.Outputable.Outputable (GHC.TypeLits.Normalise.Unify.UnifyItem v c)
instance GHC.Classes.Eq GHC.TypeLits.Normalise.Unify.CType
instance GHC.Classes.Ord GHC.TypeLits.Normalise.Unify.CType


-- | A type checker plugin for GHC that can solve <i>equalities</i> of
--   types of kind <a>Nat</a>, where these types are either:
--   
--   <ul>
--   <li>Type-level naturals</li>
--   <li>Type variables</li>
--   <li>Applications of the arithmetic expressions
--   <tt>(+,-,*,^)</tt>.</li>
--   </ul>
--   
--   It solves these equalities by normalising them to <i>sort-of</i>
--   <a>SOP</a> (Sum-of-Products) form, and then perform a simple syntactic
--   equality.
--   
--   For example, this solver can prove the equality between:
--   
--   <pre>
--   (x + 2)^(y + 2)
--   </pre>
--   
--   and
--   
--   <pre>
--   4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2
--   </pre>
--   
--   Because the latter is actually the <a>SOP</a> normal form of the
--   former.
--   
--   To use the plugin, add
--   
--   <pre>
--   {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
--   </pre>
--   
--   To the header of your file.
--   
--   <h2>Treating subtraction as addition with a negated number</h2>
--   
--   If you are absolutely sure that your subtractions can <i>never</i>
--   lead to (a locally) negative number, you can ask the plugin to treat
--   subtraction as addition with a negated operand by additionally adding:
--   
--   <pre>
--   {-# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers #-}
--   </pre>
--   
--   to the header of your file, thereby allowing to use associativity and
--   commutativity rules when proving constraints involving subtractions.
--   Note that this option can lead to unsound behaviour and should be
--   handled with extreme care.
--   
--   <h3>When it leads to unsound behaviour</h3>
--   
--   For example, enabling the <i>allow-negated-numbers</i> feature would
--   allow you to prove:
--   
--   <pre>
--   (n - 1) + 1 ~ n
--   </pre>
--   
--   <i>without</i> a <tt>(1 &lt;= n)</tt> constraint, even though when
--   <i>n</i> is set to <i>0</i> the subtraction <tt>n-1</tt> would be
--   locally negative and hence not be a natural number.
--   
--   This would allow the following erroneous definition:
--   
--   <pre>
--   data Fin (n :: Nat) where
--     FZ :: Fin (n + 1)
--     FS :: Fin n -&gt; Fin (n + 1)
--   
--   f :: forall n . Natural -&gt; Fin n
--   f n = case of
--     0 -&gt; FZ
--     x -&gt; FS (f @(n-1) (x - 1))
--   
--   fs :: [Fin 0]
--   fs = f &lt;$&gt; [0..]
--   </pre>
--   
--   <h3>When it might be Okay</h3>
--   
--   This example is taken from the <a>mezzo</a> library.
--   
--   When you have:
--   
--   <pre>
--   -- | Singleton type for the number of repetitions of an element.
--   data Times (n :: Nat) where
--       T :: Times n
--   
--   -- | An element of a "run-length encoded" vector, containing the value and
--   -- the number of repetitions
--   data Elem :: Type -&gt; Nat -&gt; Type where
--       (:*) :: t -&gt; Times n -&gt; Elem t n
--   
--   -- | A length-indexed vector, optimised for repetitions.
--   data OptVector :: Type -&gt; Nat -&gt; Type where
--       End  :: OptVector t 0
--       (:-) :: Elem t l -&gt; OptVector t (n - l) -&gt; OptVector t n
--   </pre>
--   
--   And you want to define:
--   
--   <pre>
--   -- | Append two optimised vectors.
--   type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where
--       ys        ++ End = ys
--       End       ++ ys = ys
--       (x :- xs) ++ ys = x :- (xs ++ ys)
--   </pre>
--   
--   then the last line will give rise to the constraint:
--   
--   <pre>
--   (n-l)+m ~ (n+m)-l
--   </pre>
--   
--   because:
--   
--   <pre>
--   x  :: Elem t l
--   xs :: OptVector t (n-l)
--   ys :: OptVector t m
--   </pre>
--   
--   In this case it's okay to add
--   
--   <pre>
--   {-# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers #-}
--   </pre>
--   
--   if you can convince yourself you will never be able to construct a:
--   
--   <pre>
--   xs :: OptVector t (n-l)
--   </pre>
--   
--   where <i>n-l</i> is a negative number.
module GHC.TypeLits.Normalise

-- | To use the plugin, add
--   
--   <pre>
--   {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
--   </pre>
--   
--   To the header of your file.
plugin :: Plugin
instance GHC.Utils.Outputable.Outputable GHC.TypeLits.Normalise.SimplifyResult
