{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

{-|
Module           : What4.SpecialFunctions
Description      : Utilities relating to special functions
Copyright        : (c) Galois, Inc 2021
License          : BSD3
Maintainer       : Rob Dockins <rdockins@galois.com>

Utilties for representing and handling certain \"special\"
functions arising from analysis. Although many of these
functions are most properly understood as complex valued
functions on complex arguments, here we are primarily interested
in their restriction to real-valued functions or their
floating-point approximations.

The functions considered here include functions from
standard and hyperbolic trigonometry, exponential
and logarithmic functions, etc.  Some of these functions
are defineable in terms of others (e.g. @tan(x) = sin(x)/cos(x)@
or expm1(x) = exp(x) - 1@) but are commonly implemented
separately in math libraries for increased precision.
Some popular constant values are also included.
-}

module What4.SpecialFunctions
  ( -- * Representation of special functions
    R
  , SpecialFunction(..)

    -- ** Symmetry properties of special functions
  , FunctionSymmetry(..)
  , specialFnSymmetry

    -- ** Packaging arguments to special functions
  , SpecialFnArg(..)
  , traverseSpecialFnArg
  , SpecialFnArgs(..)
  , traverseSpecialFnArgs

    -- ** Interval data for domain and range
  , RealPoint(..)
  , RealBound(..)
  , RealInterval(..)
  , specialFnDomain
  , specialFnRange
  ) where

import           Data.Kind (Type)
import           Data.Parameterized.Classes
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Context ( pattern (:>) )
import           Data.Parameterized.Ctx
import           Data.Parameterized.TH.GADT
import           Data.Parameterized.TraversableFC

-- | Some special functions exhibit useful symmetries in their arguments.
--   A function @f@ is an odd function if @f(-x) = -f(x)@, and is even
--   if @f(-x) = f(x)@.  We extend this notion to arguments of more than
--   one function by saying that a function is even/odd in its @i@th
--   argument if it is even/odd when the other arguments are fixed.
data FunctionSymmetry r
  = NoSymmetry
  | EvenFunction
  | OddFunction
 deriving (Int -> FunctionSymmetry r -> ShowS
[FunctionSymmetry r] -> ShowS
FunctionSymmetry r -> String
(Int -> FunctionSymmetry r -> ShowS)
-> (FunctionSymmetry r -> String)
-> ([FunctionSymmetry r] -> ShowS)
-> Show (FunctionSymmetry r)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (r :: k). Int -> FunctionSymmetry r -> ShowS
forall k (r :: k). [FunctionSymmetry r] -> ShowS
forall k (r :: k). FunctionSymmetry r -> String
showList :: [FunctionSymmetry r] -> ShowS
$cshowList :: forall k (r :: k). [FunctionSymmetry r] -> ShowS
show :: FunctionSymmetry r -> String
$cshow :: forall k (r :: k). FunctionSymmetry r -> String
showsPrec :: Int -> FunctionSymmetry r -> ShowS
$cshowsPrec :: forall k (r :: k). Int -> FunctionSymmetry r -> ShowS
Show)


-- | Phantom data index representing the real number line.
--   Used for specifying the arity of special functions.
data R

-- | Data type for representing \"special\" functions.
--   These include functions from standard and hyperbolic
--   trigonometry, exponential and logarithmic functions,
--   as well as other well-known mathematical functions.
--
--   Generally, little solver support exists for such functions
--   (although systems like dReal and Metatarski can prove some
--   properties).  Nonetheless, we may have some information about
--   specific values these functions take, the domains on which they
--   are defined, or the range of values their outputs may take, or
--   specific relationships that may exists between these functions
--   (e.g., trig identities).  This information may, in some
--   circumstances, be sufficent to prove properties of interest, even
--   if the functions cannot be represented in their entirety.
data SpecialFunction (args :: Ctx Type) where
  -- constant values involving Pi
  Pi             :: SpecialFunction EmptyCtx -- pi
  HalfPi         :: SpecialFunction EmptyCtx -- pi/2
  QuarterPi      :: SpecialFunction EmptyCtx -- pi/4
  OneOverPi      :: SpecialFunction EmptyCtx -- 1/pi
  TwoOverPi      :: SpecialFunction EmptyCtx -- 2/pi
  TwoOverSqrt_Pi :: SpecialFunction EmptyCtx -- 2/sqrt(pi)

  -- constant root values
  Sqrt_2         :: SpecialFunction EmptyCtx -- sqrt(2)
  Sqrt_OneHalf   :: SpecialFunction EmptyCtx -- sqrt(1/2)

  -- constant values involving exponentials and logarithms
  E              :: SpecialFunction EmptyCtx  -- e = exp(1)
  Log2_E         :: SpecialFunction EmptyCtx  -- log_2(e)
  Log10_E        :: SpecialFunction EmptyCtx  -- log_10(e)
  Ln_2           :: SpecialFunction EmptyCtx  -- ln(2)
  Ln_10          :: SpecialFunction EmptyCtx  -- ln(10)

  -- circular trigonometry functions
  Sin    :: SpecialFunction (EmptyCtx ::> R) -- sin(x)
  Cos    :: SpecialFunction (EmptyCtx ::> R) -- cos(x)
  Tan    :: SpecialFunction (EmptyCtx ::> R) -- tan(x) = sin(x)/cos(x)
  Arcsin :: SpecialFunction (EmptyCtx ::> R) -- inverse sin
  Arccos :: SpecialFunction (EmptyCtx ::> R) -- inverse cos
  Arctan :: SpecialFunction (EmptyCtx ::> R) -- inverse tan

  -- hyperbolic trigonometry functions
  Sinh    :: SpecialFunction (EmptyCtx ::> R) -- sinh(x) (hyperbolic sine)
  Cosh    :: SpecialFunction (EmptyCtx ::> R) -- cosh(x)
  Tanh    :: SpecialFunction (EmptyCtx ::> R) -- tanh(x)
  Arcsinh :: SpecialFunction (EmptyCtx ::> R) -- inverse sinh
  Arccosh :: SpecialFunction (EmptyCtx ::> R) -- inverse cosh
  Arctanh :: SpecialFunction (EmptyCtx ::> R) -- inverse tanh

  -- rectangular to polar coordinate conversion
  Hypot   :: SpecialFunction (EmptyCtx ::> R ::> R) -- hypot(x,y) = sqrt(x^2 + y^2)
  Arctan2 :: SpecialFunction (EmptyCtx ::> R ::> R) -- atan2(y,x) = atan(y/x)

  -- exponential and logarithm functions
  Pow     :: SpecialFunction (EmptyCtx ::> R ::> R) -- x^y
  Exp     :: SpecialFunction (EmptyCtx ::> R) -- exp(x)
  Log     :: SpecialFunction (EmptyCtx ::> R) -- ln(x)
  Expm1   :: SpecialFunction (EmptyCtx ::> R) -- exp(x) - 1
  Log1p   :: SpecialFunction (EmptyCtx ::> R) -- ln(1+x)

  -- base 2 exponential and logarithm
  Exp2    :: SpecialFunction (EmptyCtx ::> R) -- 2^x
  Log2    :: SpecialFunction (EmptyCtx ::> R) -- log_2(x)

  -- base 10 exponential and logarithm
  Exp10   :: SpecialFunction (EmptyCtx ::> R) -- 10^x
  Log10   :: SpecialFunction (EmptyCtx ::> R) -- log_10(x)

instance Show (SpecialFunction args) where
  show :: SpecialFunction args -> String
show SpecialFunction args
fn = case SpecialFunction args
fn of
    SpecialFunction args
Pi             -> String
"pi"
    SpecialFunction args
HalfPi         -> String
"halfPi"
    SpecialFunction args
QuarterPi      -> String
"quaterPi"
    SpecialFunction args
OneOverPi      -> String
"oneOverPi"
    SpecialFunction args
TwoOverPi      -> String
"twoOverPi"
    SpecialFunction args
TwoOverSqrt_Pi -> String
"twoOverSqrt_Pi"
    SpecialFunction args
Sqrt_2         -> String
"sqrt_2"
    SpecialFunction args
Sqrt_OneHalf   -> String
"sqrt_oneHalf"

    SpecialFunction args
E              -> String
"e"
    SpecialFunction args
Log2_E         -> String
"log2_e"
    SpecialFunction args
Log10_E        -> String
"log10_e"
    SpecialFunction args
Ln_2           -> String
"ln_2"
    SpecialFunction args
Ln_10          -> String
"ln_10"

    SpecialFunction args
Sin            -> String
"sin"
    SpecialFunction args
Cos            -> String
"cos"
    SpecialFunction args
Tan            -> String
"tan"
    SpecialFunction args
Arcsin         -> String
"arcsin"
    SpecialFunction args
Arccos         -> String
"arccos"
    SpecialFunction args
Arctan         -> String
"arctan"

    SpecialFunction args
Sinh           -> String
"sinh"
    SpecialFunction args
Cosh           -> String
"cosh"
    SpecialFunction args
Tanh           -> String
"tanh"
    SpecialFunction args
Arcsinh        -> String
"arcsinh"
    SpecialFunction args
Arccosh        -> String
"arccosh"
    SpecialFunction args
Arctanh        -> String
"arctanh"

    SpecialFunction args
Hypot          -> String
"hypot"
    SpecialFunction args
Arctan2        -> String
"atan2"

    SpecialFunction args
Pow            -> String
"pow"
    SpecialFunction args
Exp            -> String
"exp"
    SpecialFunction args
Log            -> String
"ln"
    SpecialFunction args
Expm1          -> String
"expm1"
    SpecialFunction args
Log1p          -> String
"log1p"
    SpecialFunction args
Exp2           -> String
"exp2"
    SpecialFunction args
Log2           -> String
"log2"
    SpecialFunction args
Exp10          -> String
"exp10"
    SpecialFunction args
Log10          -> String
"log10"

-- | Values that can appear in the definition of domain and
--   range intervals for special functions.
data RealPoint
  = Zero
  | NegOne
  | PosOne
  | NegInf
  | PosInf
  | NegPi
  | PosPi
  | NegHalfPi
  | PosHalfPi

instance Show RealPoint where
  show :: RealPoint -> String
show RealPoint
Zero   = String
"0"
  show RealPoint
NegOne = String
"-1"
  show RealPoint
PosOne = String
"+1"
  show RealPoint
NegInf = String
"-∞"
  show RealPoint
PosInf = String
"+∞"
  show RealPoint
NegPi  = String
"-π"
  show RealPoint
PosPi  = String
"+π"
  show RealPoint
NegHalfPi = String
"-π/2"
  show RealPoint
PosHalfPi = String
"+π/2"

-- | The endpoint of an interval, which may be inclusive or exclusive.
data RealBound
  = Incl RealPoint
  | Excl RealPoint

-- | An interval on real values, or a point.
data RealInterval r where
  RealPoint    :: SpecialFunction EmptyCtx -> RealInterval R
  RealInterval :: RealBound -> RealBound -> RealInterval R

instance Show (RealInterval r) where
  show :: RealInterval r -> String
show (RealPoint SpecialFunction EmptyCtx
x) = SpecialFunction EmptyCtx -> String
forall a. Show a => a -> String
show SpecialFunction EmptyCtx
x
  show (RealInterval RealBound
lo RealBound
hi) = String
lostr String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
histr
    where
      lostr :: String
lostr = case RealBound
lo of
                Incl RealPoint
x -> String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ RealPoint -> String
forall a. Show a => a -> String
show RealPoint
x
                Excl RealPoint
x -> String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ RealPoint -> String
forall a. Show a => a -> String
show RealPoint
x
      histr :: String
histr = case RealBound
hi of
                Incl RealPoint
x -> RealPoint -> String
forall a. Show a => a -> String
show RealPoint
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
                Excl RealPoint
x -> RealPoint -> String
forall a. Show a => a -> String
show RealPoint
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

-- | Compute function symmetry information for the given special function.
specialFnSymmetry :: SpecialFunction args -> Ctx.Assignment FunctionSymmetry args
specialFnSymmetry :: SpecialFunction args -> Assignment FunctionSymmetry args
specialFnSymmetry SpecialFunction args
fn = case SpecialFunction args
fn of
    SpecialFunction args
Pi             -> Assignment FunctionSymmetry args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
HalfPi         -> Assignment FunctionSymmetry args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
QuarterPi      -> Assignment FunctionSymmetry args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
OneOverPi      -> Assignment FunctionSymmetry args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
TwoOverPi      -> Assignment FunctionSymmetry args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
TwoOverSqrt_Pi -> Assignment FunctionSymmetry args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
Sqrt_2         -> Assignment FunctionSymmetry args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
Sqrt_OneHalf   -> Assignment FunctionSymmetry args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
E              -> Assignment FunctionSymmetry args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
Log2_E         -> Assignment FunctionSymmetry args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
Log10_E        -> Assignment FunctionSymmetry args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
Ln_2           -> Assignment FunctionSymmetry args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
Ln_10          -> Assignment FunctionSymmetry args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty

    SpecialFunction args
Sin            -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
OddFunction
    SpecialFunction args
Cos            -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
EvenFunction
    SpecialFunction args
Tan            -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
OddFunction
    SpecialFunction args
Arcsin         -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
OddFunction
    SpecialFunction args
Arccos         -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
NoSymmetry
    SpecialFunction args
Arctan         -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
OddFunction

    SpecialFunction args
Sinh           -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
OddFunction
    SpecialFunction args
Cosh           -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
EvenFunction
    SpecialFunction args
Tanh           -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
OddFunction
    SpecialFunction args
Arcsinh        -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
OddFunction
    SpecialFunction args
Arccosh        -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
NoSymmetry
    SpecialFunction args
Arctanh        -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
OddFunction

    SpecialFunction args
Pow            -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R
-> Assignment FunctionSymmetry (EmptyCtx ::> R)
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
NoSymmetry Assignment FunctionSymmetry (EmptyCtx ::> R)
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
NoSymmetry
    SpecialFunction args
Exp            -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
NoSymmetry
    SpecialFunction args
Log            -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
NoSymmetry
    SpecialFunction args
Expm1          -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
NoSymmetry
    SpecialFunction args
Log1p          -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
NoSymmetry
    SpecialFunction args
Exp2           -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
NoSymmetry
    SpecialFunction args
Log2           -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
NoSymmetry
    SpecialFunction args
Exp10          -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
NoSymmetry
    SpecialFunction args
Log10          -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
NoSymmetry

    SpecialFunction args
Hypot          -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R
-> Assignment FunctionSymmetry (EmptyCtx ::> R)
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
EvenFunction Assignment FunctionSymmetry (EmptyCtx ::> R)
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
EvenFunction
    SpecialFunction args
Arctan2        -> Assignment FunctionSymmetry EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment FunctionSymmetry EmptyCtx
-> FunctionSymmetry R
-> Assignment FunctionSymmetry (EmptyCtx ::> R)
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
OddFunction Assignment FunctionSymmetry (EmptyCtx ::> R)
-> FunctionSymmetry R -> Assignment FunctionSymmetry args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> FunctionSymmetry R
forall k (r :: k). FunctionSymmetry r
NoSymmetry


-- | Compute the range of values that may be returned by the given special function
--   as its arguments take on the possible values of its domain.  This may include
--   limiting values if the function's domain includes infinities; for example
--   @exp(-inf) = 0@.
specialFnRange :: SpecialFunction args -> RealInterval R
specialFnRange :: SpecialFunction args -> RealInterval R
specialFnRange SpecialFunction args
fn = case SpecialFunction args
fn of
    SpecialFunction args
Pi             -> SpecialFunction EmptyCtx -> RealInterval R
RealPoint SpecialFunction EmptyCtx
Pi
    SpecialFunction args
HalfPi         -> SpecialFunction EmptyCtx -> RealInterval R
RealPoint SpecialFunction EmptyCtx
HalfPi
    SpecialFunction args
QuarterPi      -> SpecialFunction EmptyCtx -> RealInterval R
RealPoint SpecialFunction EmptyCtx
QuarterPi
    SpecialFunction args
OneOverPi      -> SpecialFunction EmptyCtx -> RealInterval R
RealPoint SpecialFunction EmptyCtx
OneOverPi
    SpecialFunction args
TwoOverPi      -> SpecialFunction EmptyCtx -> RealInterval R
RealPoint SpecialFunction EmptyCtx
TwoOverPi
    SpecialFunction args
TwoOverSqrt_Pi -> SpecialFunction EmptyCtx -> RealInterval R
RealPoint SpecialFunction EmptyCtx
TwoOverSqrt_Pi
    SpecialFunction args
Sqrt_2         -> SpecialFunction EmptyCtx -> RealInterval R
RealPoint SpecialFunction EmptyCtx
Sqrt_2
    SpecialFunction args
Sqrt_OneHalf   -> SpecialFunction EmptyCtx -> RealInterval R
RealPoint SpecialFunction EmptyCtx
Sqrt_OneHalf
    SpecialFunction args
E              -> SpecialFunction EmptyCtx -> RealInterval R
RealPoint SpecialFunction EmptyCtx
E
    SpecialFunction args
Log2_E         -> SpecialFunction EmptyCtx -> RealInterval R
RealPoint SpecialFunction EmptyCtx
Log2_E
    SpecialFunction args
Log10_E        -> SpecialFunction EmptyCtx -> RealInterval R
RealPoint SpecialFunction EmptyCtx
Log10_E
    SpecialFunction args
Ln_2           -> SpecialFunction EmptyCtx -> RealInterval R
RealPoint SpecialFunction EmptyCtx
Ln_2
    SpecialFunction args
Ln_10          -> SpecialFunction EmptyCtx -> RealInterval R
RealPoint SpecialFunction EmptyCtx
Ln_10

    SpecialFunction args
Sin            -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegOne) (RealPoint -> RealBound
Incl RealPoint
PosOne)
    SpecialFunction args
Cos            -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegOne) (RealPoint -> RealBound
Incl RealPoint
PosOne)
    SpecialFunction args
Tan            -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)

    SpecialFunction args
Arcsin         -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegHalfPi) (RealPoint -> RealBound
Incl RealPoint
PosHalfPi)
    SpecialFunction args
Arccos         -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
Zero)      (RealPoint -> RealBound
Incl RealPoint
PosPi)
    SpecialFunction args
Arctan         -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegHalfPi) (RealPoint -> RealBound
Incl RealPoint
PosHalfPi)

    SpecialFunction args
Sinh           -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Cosh           -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
PosOne) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Tanh           -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegOne) (RealPoint -> RealBound
Incl RealPoint
PosOne)
    SpecialFunction args
Arcsinh        -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Arccosh        -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
Zero)   (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Arctanh        -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)

    SpecialFunction args
Pow            -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Exp            -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
Zero)   (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Log            -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Expm1          -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegOne) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Log1p          -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Exp2           -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
Zero)   (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Log2           -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Exp10          -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
Zero)   (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Log10          -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)

    SpecialFunction args
Hypot          -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
Zero) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Arctan2        -> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegPi) (RealPoint -> RealBound
Incl RealPoint
PosPi)


-- | Compute the domain of the given special function.  As a mathematical
--   entity, the value of the given function is not well-defined outside
--   its domain. In floating-point terms, a special function will return
--   a @NaN@ when evaluated on arguments outside its domain.
specialFnDomain :: SpecialFunction args -> Ctx.Assignment RealInterval args
specialFnDomain :: SpecialFunction args -> Assignment RealInterval args
specialFnDomain SpecialFunction args
fn = case SpecialFunction args
fn of
    SpecialFunction args
Pi             -> Assignment RealInterval args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
HalfPi         -> Assignment RealInterval args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
QuarterPi      -> Assignment RealInterval args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
OneOverPi      -> Assignment RealInterval args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
TwoOverPi      -> Assignment RealInterval args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
TwoOverSqrt_Pi -> Assignment RealInterval args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
Sqrt_2         -> Assignment RealInterval args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
Sqrt_OneHalf   -> Assignment RealInterval args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
E              -> Assignment RealInterval args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
Log2_E         -> Assignment RealInterval args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
Log10_E        -> Assignment RealInterval args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
Ln_2           -> Assignment RealInterval args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
    SpecialFunction args
Ln_10          -> Assignment RealInterval args
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty

    SpecialFunction args
Sin            -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Excl RealPoint
NegInf) (RealPoint -> RealBound
Excl RealPoint
PosInf)
    SpecialFunction args
Cos            -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Excl RealPoint
NegInf) (RealPoint -> RealBound
Excl RealPoint
PosInf)
    SpecialFunction args
Tan            -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Excl RealPoint
NegInf) (RealPoint -> RealBound
Excl RealPoint
PosInf)
    SpecialFunction args
Arcsin         -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegOne) (RealPoint -> RealBound
Incl RealPoint
PosOne)
    SpecialFunction args
Arccos         -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegOne) (RealPoint -> RealBound
Incl RealPoint
PosOne)
    SpecialFunction args
Arctan         -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)

    SpecialFunction args
Sinh           -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Cosh           -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Tanh           -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Arcsinh        -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Arccosh        -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
PosOne) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Arctanh        -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegOne) (RealPoint -> RealBound
Incl RealPoint
PosOne)

    SpecialFunction args
Pow            -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval (EmptyCtx ::> R)
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
                                Assignment RealInterval (EmptyCtx ::> R)
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Exp            -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Log            -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
Zero)   (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Expm1          -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Log1p          -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegOne) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Exp2           -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Log2           -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
Zero)   (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Exp10          -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Log10          -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
Zero)   (RealPoint -> RealBound
Incl RealPoint
PosInf)

    SpecialFunction args
Hypot          -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval (EmptyCtx ::> R)
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
                                Assignment RealInterval (EmptyCtx ::> R)
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
    SpecialFunction args
Arctan2        -> Assignment RealInterval EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty Assignment RealInterval EmptyCtx
-> RealInterval R -> Assignment RealInterval (EmptyCtx ::> R)
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)
                                Assignment RealInterval (EmptyCtx ::> R)
-> RealInterval R -> Assignment RealInterval args
forall k (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> RealBound -> RealBound -> RealInterval R
RealInterval (RealPoint -> RealBound
Incl RealPoint
NegInf) (RealPoint -> RealBound
Incl RealPoint
PosInf)

-- | Data type for wrapping the actual arguments to special functions.
data SpecialFnArg (e :: k -> Type) (tp::k) (r::Type) where
  SpecialFnArg :: e tp -> SpecialFnArg e tp R

-- | Data type for wrapping a collction of actual arguments to special functions.
newtype SpecialFnArgs (e :: k -> Type) (tp :: k) args =
  SpecialFnArgs (Ctx.Assignment (SpecialFnArg e tp) args)

$(return [])

instance HashableF SpecialFunction where
  hashWithSaltF :: Int -> SpecialFunction tp -> Int
hashWithSaltF = $(structuralHashWithSalt [t|SpecialFunction|] [])

instance Hashable (SpecialFunction args) where
  hashWithSalt :: Int -> SpecialFunction args -> Int
hashWithSalt = Int -> SpecialFunction args -> Int
forall k (f :: k -> Type) (tp :: k).
HashableF f =>
Int -> f tp -> Int
hashWithSaltF

instance TestEquality SpecialFunction where
  testEquality :: SpecialFunction a -> SpecialFunction b -> Maybe (a :~: b)
testEquality = $(structuralTypeEquality [t|SpecialFunction|] [])

instance Eq (SpecialFunction args) where
  SpecialFunction args
x == :: SpecialFunction args -> SpecialFunction args -> Bool
== SpecialFunction args
y = Maybe (args :~: args) -> Bool
forall a. Maybe a -> Bool
isJust (SpecialFunction args
-> SpecialFunction args -> Maybe (args :~: args)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SpecialFunction args
x SpecialFunction args
y)

instance OrdF SpecialFunction where
  compareF :: SpecialFunction x -> SpecialFunction y -> OrderingF x y
compareF = $(structuralTypeOrd [t|SpecialFunction|] [])


instance OrdF e => TestEquality (SpecialFnArg e tp) where
  testEquality :: SpecialFnArg e tp a -> SpecialFnArg e tp b -> Maybe (a :~: b)
testEquality (SpecialFnArg e tp
x) (SpecialFnArg e tp
y) =
    do tp :~: tp
Refl <- e tp -> e tp -> Maybe (tp :~: tp)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality e tp
x e tp
y
       (a :~: a) -> Maybe (a :~: a)
forall (m :: Type -> Type) a. Monad m => a -> m a
return a :~: a
forall k (a :: k). a :~: a
Refl

instance OrdF e => OrdF (SpecialFnArg e tp) where
  compareF :: SpecialFnArg e tp x -> SpecialFnArg e tp y -> OrderingF x y
compareF (SpecialFnArg e tp
x) (SpecialFnArg e tp
y) =
    case e tp -> e tp -> OrderingF tp tp
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF e tp
x e tp
y of
      OrderingF tp tp
LTF -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
LTF
      OrderingF tp tp
EQF -> OrderingF x y
forall k (x :: k). OrderingF x x
EQF
      OrderingF tp tp
GTF -> OrderingF x y
forall k (x :: k) (y :: k). OrderingF x y
GTF

instance HashableF e => HashableF (SpecialFnArg e tp) where
  hashWithSaltF :: Int -> SpecialFnArg e tp tp -> Int
hashWithSaltF Int
s (SpecialFnArg e tp
x) = Int -> e tp -> Int
forall k (f :: k -> Type) (tp :: k).
HashableF f =>
Int -> f tp -> Int
hashWithSaltF Int
s e tp
x


instance OrdF e => Eq (SpecialFnArgs e tp r) where
  SpecialFnArgs Assignment (SpecialFnArg e tp) r
xs == :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Bool
== SpecialFnArgs Assignment (SpecialFnArg e tp) r
ys = Assignment (SpecialFnArg e tp) r
xs Assignment (SpecialFnArg e tp) r
-> Assignment (SpecialFnArg e tp) r -> Bool
forall a. Eq a => a -> a -> Bool
== Assignment (SpecialFnArg e tp) r
ys

instance OrdF e => Ord (SpecialFnArgs e tp r) where
  compare :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Ordering
compare (SpecialFnArgs Assignment (SpecialFnArg e tp) r
xs) (SpecialFnArgs Assignment (SpecialFnArg e tp) r
ys) = Assignment (SpecialFnArg e tp) r
-> Assignment (SpecialFnArg e tp) r -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Assignment (SpecialFnArg e tp) r
xs Assignment (SpecialFnArg e tp) r
ys

instance (HashableF e, OrdF e) => Hashable (SpecialFnArgs e tp args) where
  hashWithSalt :: Int -> SpecialFnArgs e tp args -> Int
hashWithSalt Int
s (SpecialFnArgs Assignment (SpecialFnArg e tp) args
xs) = Int -> Assignment (SpecialFnArg e tp) args -> Int
forall k (f :: k -> Type) (tp :: k).
HashableF f =>
Int -> f tp -> Int
hashWithSaltF Int
s Assignment (SpecialFnArg e tp) args
xs


traverseSpecialFnArg :: Applicative m =>
  (e tp -> m (f tp)) ->
  SpecialFnArg e tp r -> m (SpecialFnArg f tp r)
traverseSpecialFnArg :: (e tp -> m (f tp))
-> SpecialFnArg e tp r -> m (SpecialFnArg f tp r)
traverseSpecialFnArg e tp -> m (f tp)
f (SpecialFnArg e tp
x) = f tp -> SpecialFnArg f tp R
forall k (e :: k -> Type) (tp :: k). e tp -> SpecialFnArg e tp R
SpecialFnArg (f tp -> SpecialFnArg f tp R)
-> m (f tp) -> m (SpecialFnArg f tp R)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> e tp -> m (f tp)
f e tp
x

traverseSpecialFnArgs :: Applicative m =>
  (e tp -> m (f tp)) ->
  SpecialFnArgs e tp r -> m (SpecialFnArgs f tp r)
traverseSpecialFnArgs :: (e tp -> m (f tp))
-> SpecialFnArgs e tp r -> m (SpecialFnArgs f tp r)
traverseSpecialFnArgs e tp -> m (f tp)
f (SpecialFnArgs Assignment (SpecialFnArg e tp) r
xs) =
  Assignment (SpecialFnArg f tp) r -> SpecialFnArgs f tp r
forall k (e :: k -> Type) (tp :: k) (args :: Ctx Type).
Assignment (SpecialFnArg e tp) args -> SpecialFnArgs e tp args
SpecialFnArgs (Assignment (SpecialFnArg f tp) r -> SpecialFnArgs f tp r)
-> m (Assignment (SpecialFnArg f tp) r) -> m (SpecialFnArgs f tp r)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall x. SpecialFnArg e tp x -> m (SpecialFnArg f tp x))
-> Assignment (SpecialFnArg e tp) r
-> m (Assignment (SpecialFnArg f tp) r)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC ((e tp -> m (f tp))
-> SpecialFnArg e tp x -> m (SpecialFnArg f tp x)
forall k (m :: Type -> Type) (e :: k -> Type) (tp :: k)
       (f :: k -> Type) r.
Applicative m =>
(e tp -> m (f tp))
-> SpecialFnArg e tp r -> m (SpecialFnArg f tp r)
traverseSpecialFnArg e tp -> m (f tp)
f) Assignment (SpecialFnArg e tp) r
xs