{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module What4.SpecialFunctions
(
R
, SpecialFunction(..)
, FunctionSymmetry(..)
, specialFnSymmetry
, SpecialFnArg(..)
, traverseSpecialFnArg
, SpecialFnArgs(..)
, traverseSpecialFnArgs
, 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
data FunctionSymmetry r
= NoSymmetry
| EvenFunction
| OddFunction
deriving (Int -> FunctionSymmetry r -> ShowS
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)
data R
data SpecialFunction (args :: Ctx Type) where
Pi :: SpecialFunction EmptyCtx
HalfPi :: SpecialFunction EmptyCtx
QuarterPi :: SpecialFunction EmptyCtx
OneOverPi :: SpecialFunction EmptyCtx
TwoOverPi :: SpecialFunction EmptyCtx
TwoOverSqrt_Pi :: SpecialFunction EmptyCtx
Sqrt_2 :: SpecialFunction EmptyCtx
Sqrt_OneHalf :: SpecialFunction EmptyCtx
E :: SpecialFunction EmptyCtx
Log2_E :: SpecialFunction EmptyCtx
Log10_E :: SpecialFunction EmptyCtx
Ln_2 :: SpecialFunction EmptyCtx
Ln_10 :: SpecialFunction EmptyCtx
Sin :: SpecialFunction (EmptyCtx ::> R)
Cos :: SpecialFunction (EmptyCtx ::> R)
Tan :: SpecialFunction (EmptyCtx ::> R)
Arcsin :: SpecialFunction (EmptyCtx ::> R)
Arccos :: SpecialFunction (EmptyCtx ::> R)
Arctan :: SpecialFunction (EmptyCtx ::> R)
Sinh :: SpecialFunction (EmptyCtx ::> R)
Cosh :: SpecialFunction (EmptyCtx ::> R)
Tanh :: SpecialFunction (EmptyCtx ::> R)
Arcsinh :: SpecialFunction (EmptyCtx ::> R)
Arccosh :: SpecialFunction (EmptyCtx ::> R)
Arctanh :: SpecialFunction (EmptyCtx ::> R)
Hypot :: SpecialFunction (EmptyCtx ::> R ::> R)
Arctan2 :: SpecialFunction (EmptyCtx ::> R ::> R)
Pow :: SpecialFunction (EmptyCtx ::> R ::> R)
Exp :: SpecialFunction (EmptyCtx ::> R)
Log :: SpecialFunction (EmptyCtx ::> R)
Expm1 :: SpecialFunction (EmptyCtx ::> R)
Log1p :: SpecialFunction (EmptyCtx ::> R)
Exp2 :: SpecialFunction (EmptyCtx ::> R)
Log2 :: SpecialFunction (EmptyCtx ::> R)
Exp10 :: SpecialFunction (EmptyCtx ::> R)
Log10 :: SpecialFunction (EmptyCtx ::> R)
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"
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"
data RealBound
= Incl RealPoint
| Excl RealPoint
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) = forall a. Show a => a -> String
show SpecialFunction 'EmptyCtx
x
show (RealInterval RealBound
lo RealBound
hi) = String
lostr forall a. [a] -> [a] -> [a]
++ String
", " forall a. [a] -> [a] -> [a]
++ String
histr
where
lostr :: String
lostr = case RealBound
lo of
Incl RealPoint
x -> String
"[" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RealPoint
x
Excl RealPoint
x -> String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RealPoint
x
histr :: String
histr = case RealBound
hi of
Incl RealPoint
x -> forall a. Show a => a -> String
show RealPoint
x forall a. [a] -> [a] -> [a]
++ String
"]"
Excl RealPoint
x -> forall a. Show a => a -> String
show RealPoint
x forall a. [a] -> [a] -> [a]
++ String
")"
specialFnSymmetry :: SpecialFunction args -> Ctx.Assignment FunctionSymmetry args
specialFnSymmetry :: forall (args :: Ctx Type).
SpecialFunction args -> Assignment FunctionSymmetry args
specialFnSymmetry SpecialFunction args
fn = case SpecialFunction args
fn of
SpecialFunction args
Pi -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
HalfPi -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
QuarterPi -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
OneOverPi -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
TwoOverPi -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
TwoOverSqrt_Pi -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
Sqrt_2 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
Sqrt_OneHalf -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
E -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
Log2_E -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
Log10_E -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
Ln_2 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
Ln_10 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
Sin -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
OddFunction
SpecialFunction args
Cos -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
EvenFunction
SpecialFunction args
Tan -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
OddFunction
SpecialFunction args
Arcsin -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
OddFunction
SpecialFunction args
Arccos -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
NoSymmetry
SpecialFunction args
Arctan -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
OddFunction
SpecialFunction args
Sinh -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
OddFunction
SpecialFunction args
Cosh -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
EvenFunction
SpecialFunction args
Tanh -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
OddFunction
SpecialFunction args
Arcsinh -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
OddFunction
SpecialFunction args
Arccosh -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
NoSymmetry
SpecialFunction args
Arctanh -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
OddFunction
SpecialFunction args
Pow -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
NoSymmetry forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
NoSymmetry
SpecialFunction args
Exp -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
NoSymmetry
SpecialFunction args
Log -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
NoSymmetry
SpecialFunction args
Expm1 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
NoSymmetry
SpecialFunction args
Log1p -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
NoSymmetry
SpecialFunction args
Exp2 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
NoSymmetry
SpecialFunction args
Log2 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
NoSymmetry
SpecialFunction args
Exp10 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
NoSymmetry
SpecialFunction args
Log10 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
NoSymmetry
SpecialFunction args
Hypot -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
EvenFunction forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
EvenFunction
SpecialFunction args
Arctan2 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
OddFunction forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> forall {k} (r :: k). FunctionSymmetry r
NoSymmetry
specialFnRange :: SpecialFunction args -> RealInterval R
specialFnRange :: forall (args :: Ctx Type). 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)
specialFnDomain :: SpecialFunction args -> Ctx.Assignment RealInterval args
specialFnDomain :: forall (args :: Ctx Type).
SpecialFunction args -> Assignment RealInterval args
specialFnDomain SpecialFunction args
fn = case SpecialFunction args
fn of
SpecialFunction args
Pi -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
HalfPi -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
QuarterPi -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
OneOverPi -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
TwoOverPi -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
TwoOverSqrt_Pi -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
Sqrt_2 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
Sqrt_OneHalf -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
E -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
Log2_E -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
Log10_E -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
Ln_2 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
Ln_10 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty
SpecialFunction args
Sin -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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)
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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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)
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 -> forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Ctx.Empty 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)
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 SpecialFnArg (e :: k -> Type) (tp::k) (r::Type) where
SpecialFnArg :: e tp -> SpecialFnArg e tp R
newtype SpecialFnArgs (e :: k -> Type) (tp :: k) args =
SpecialFnArgs (Ctx.Assignment (SpecialFnArg e tp) args)
$(return [])
instance HashableF SpecialFunction where
hashWithSaltF :: forall (tp :: Ctx Type). Int -> SpecialFunction tp -> Int
hashWithSaltF = $(structuralHashWithSalt [t|SpecialFunction|] [])
instance Hashable (SpecialFunction args) where
hashWithSalt :: Int -> SpecialFunction args -> Int
hashWithSalt = forall k (f :: k -> Type) (tp :: k).
HashableF f =>
Int -> f tp -> Int
hashWithSaltF
instance TestEquality SpecialFunction where
testEquality :: forall (a :: Ctx Type) (b :: Ctx Type).
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 = forall a. Maybe a -> Bool
isJust (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 :: forall (x :: Ctx Type) (y :: Ctx Type).
SpecialFunction x -> SpecialFunction y -> OrderingF x y
compareF = $(structuralTypeOrd [t|SpecialFunction|] [])
instance OrdF e => TestEquality (SpecialFnArg e tp) where
testEquality :: forall a b.
SpecialFnArg e tp a -> SpecialFnArg e tp b -> Maybe (a :~: b)
testEquality (SpecialFnArg e tp
x) (SpecialFnArg e tp
y) =
do tp :~: tp
Refl <- 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
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl
instance OrdF e => OrdF (SpecialFnArg e tp) where
compareF :: forall x y.
SpecialFnArg e tp x -> SpecialFnArg e tp y -> OrderingF x y
compareF (SpecialFnArg e tp
x) (SpecialFnArg e tp
y) =
case 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 -> forall {k} (x :: k) (y :: k). OrderingF x y
LTF
OrderingF tp tp
EQF -> forall {k} (x :: k). OrderingF x x
EQF
OrderingF tp tp
GTF -> forall {k} (x :: k) (y :: k). OrderingF x y
GTF
instance HashableF e => HashableF (SpecialFnArg e tp) where
hashWithSaltF :: forall tp. Int -> SpecialFnArg e tp tp -> Int
hashWithSaltF Int
s (SpecialFnArg e tp
x) = 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 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) = 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) = 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 :: 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 (SpecialFnArg e tp
x) = forall {k} (e :: k -> Type) (tp :: k). e tp -> SpecialFnArg e tp R
SpecialFnArg 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 :: forall {k} (m :: Type -> Type) (e :: k -> Type) (tp :: k)
(f :: k -> Type) (r :: Ctx Type).
Applicative m =>
(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) =
forall k (e :: k -> Type) (tp :: k) (args :: Ctx Type).
Assignment (SpecialFnArg e tp) args -> SpecialFnArgs e tp args
SpecialFnArgs forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (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