Safe Haskell	Safe-Inferred
Language	Haskell2010

Constrained.NumSpec

Contents

Orphan instances

Synopsis

data NumOrdW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where
- LessOrEqualW ∷ OrdLike a ⇒ NumOrdW "<=." '[a, a] Bool
- LessW ∷ OrdLike a ⇒ NumOrdW "<." '[a, a] Bool
- GreaterOrEqualW ∷ OrdLike a ⇒ NumOrdW ">=." '[a, a] Bool
- GreaterW ∷ OrdLike a ⇒ NumOrdW ">." '[a, a] Bool
class (Ord a, HasSpec a) ⇒ OrdLike a where
- leqSpec ∷ a → Specification a
- ltSpec ∷ a → Specification a
- geqSpec ∷ a → Specification a
- gtSpec ∷ a → Specification a
class MaybeBounded a where
- lowerBound ∷ Maybe a
- upperBound ∷ Maybe a
data NumSpec n = NumSpecInterval (Maybe n) (Maybe n)
emptyNumSpec ∷ Ord a ⇒ NumSpec a
guardNumSpec ∷ (Ord n, HasSpec n, TypeSpec n ~ NumSpec n) ⇒ [String] → NumSpec n → Specification n
combineNumSpec ∷ (HasSpec n, Ord n, TypeSpec n ~ NumSpec n) ⇒ NumSpec n → NumSpec n → Specification n
genFromNumSpec ∷ (MonadGenError m, Show n, Random n, Ord n, Num n, MaybeBounded n) ⇒ NumSpec n → GenT m n
shrinkWithNumSpec ∷ Arbitrary n ⇒ NumSpec n → n → [n]
constrainInterval ∷ (MonadGenError m, Ord a, Num a, Show a) ⇒ Maybe a → Maybe a → Integer → m (a, a)
conformsToNumSpec ∷ Ord n ⇒ n → NumSpec n → Bool
nubOrd ∷ Ord a ⇒ [a] → [a]
nubOrdMemberSpec ∷ Ord a ⇒ String → [a] → Specification a
lowBound ∷ Bounded n ⇒ Maybe n → n
highBound ∷ Bounded n ⇒ Maybe n → n
countSpec ∷ ∀ n. (Bounded n, Integral n) ⇒ NumSpec n → Integer
finiteSize ∷ ∀ n. (Integral n, Bounded n) ⇒ Integer
notInNumSpec ∷ ∀ n. (HasSpec n, TypeSpec n ~ NumSpec n, Bounded n, Integral n) ⇒ NumSpec n → [n] → Specification n
guardEmpty ∷ (Ord n, Num n) ⇒ Maybe n → Maybe n → NumSpec n → NumSpec n
addNumSpec ∷ (Ord n, Num n) ⇒ NumSpec n → NumSpec n → NumSpec n
subNumSpec ∷ (Ord n, Num n) ⇒ NumSpec n → NumSpec n → NumSpec n
multNumSpec ∷ (Ord n, Num n) ⇒ NumSpec n → NumSpec n → NumSpec n
negNumSpec ∷ Num n ⇒ NumSpec n → NumSpec n
data T x
- = NegInf
- | Ok x
- | PosInf
unT ∷ T x → Maybe x
neg ∷ Maybe x → T x
pos ∷ Maybe x → T x
multT ∷ Num x ⇒ T x → T x → T x
type Number n = (Num n, Enum n, TypeSpec n ~ NumSpec n, Num (NumSpec n), HasSpec n, Ord n)
addSpecInt ∷ Number n ⇒ Specification n → Specification n → Specification n
subSpecInt ∷ Number n ⇒ Specification n → Specification n → Specification n
multSpecInt ∷ Number n ⇒ Specification n → Specification n → Specification n
operateSpec ∷ Number n ⇒ String → (n → n → n) → (TypeSpec n → TypeSpec n → TypeSpec n) → Specification n → Specification n → Specification n
cardinality ∷ ∀ a. (Number Integer, HasSpec a) ⇒ Specification a → Specification Integer
cardinalNumSpec ∷ ∀ n. (Integral n, MaybeBounded n) ⇒ NumSpec n → Specification Integer
class (Num a, HasSpec a) ⇒ NumLike a where
- subtractSpec ∷ a → TypeSpec a → Specification a
- negateSpec ∷ TypeSpec a → Specification a
- safeSubtract ∷ a → a → Maybe a
data IntW (s ∷ Symbol) (as ∷ [Type]) b where
- AddW ∷ NumLike a ⇒ IntW "addFn" '[a, a] a
- NegateW ∷ NumLike a ⇒ IntW "negateFn" '[a] a
type Numeric a = (HasSpec a, Ord a, Num a, TypeSpec a ~ NumSpec a, MaybeBounded a)
addFn ∷ ∀ a. NumLike a ⇒ Term a → Term a → Term a
negateFn ∷ ∀ a. NumLike a ⇒ Term a → Term a

Documentation

data NumOrdW (sym ∷ Symbol) (dom ∷ [Type]) (rng ∷ Type) where Source #

Constructors

LessOrEqualW ∷ OrdLike a ⇒ NumOrdW "<=." '[a, a] Bool
LessW ∷ OrdLike a ⇒ NumOrdW "<." '[a, a] Bool
GreaterOrEqualW ∷ OrdLike a ⇒ NumOrdW ">=." '[a, a] Bool
GreaterW ∷ OrdLike a ⇒ NumOrdW ">." '[a, a] Bool

Instances

Instances details

Semantics NumOrdW Source #
Instance details Defined in Constrained.NumSpec Methods semantics ∷ ∀ (s ∷ Symbol) (d ∷ [Type]) r. NumOrdW s d r → FunTy d r Source #
Syntax NumOrdW Source #
Instance details Defined in Constrained.NumSpec Methods isInFix ∷ ∀ (s ∷ Symbol) (dom ∷ [Type]) rng. NumOrdW s dom rng → Bool Source # prettyWit ∷ ∀ (s ∷ Symbol) (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ NumOrdW s dom rng → List Term dom → Int → Maybe (Doc ann) Source #
OrdLike a ⇒ Logic "<." NumOrdW '[a, a] Bool Source #
Instance details Defined in Constrained.TheKnot Methods info ∷ NumOrdW "<." '[a, a] Bool → String Source # propagate ∷ Context "<." NumOrdW '[a, a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ NumOrdW "<." '[a, a] Bool → List Term '[a, a] → Evidence (AppRequires "<." NumOrdW '[a, a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ NumOrdW "<." '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ NumOrdW "<." '[a, a] Bool → List Term '[a, a] → [Pred] Source #
OrdLike a ⇒ Logic "<=." NumOrdW '[a, a] Bool Source #
Instance details Defined in Constrained.TheKnot Methods info ∷ NumOrdW "<=." '[a, a] Bool → String Source # propagate ∷ Context "<=." NumOrdW '[a, a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ NumOrdW "<=." '[a, a] Bool → List Term '[a, a] → Evidence (AppRequires "<=." NumOrdW '[a, a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ NumOrdW "<=." '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ NumOrdW "<=." '[a, a] Bool → List Term '[a, a] → [Pred] Source #
OrdLike a ⇒ Logic ">." NumOrdW '[a, a] Bool Source #
Instance details Defined in Constrained.TheKnot Methods info ∷ NumOrdW ">." '[a, a] Bool → String Source # propagate ∷ Context ">." NumOrdW '[a, a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ NumOrdW ">." '[a, a] Bool → List Term '[a, a] → Evidence (AppRequires ">." NumOrdW '[a, a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ NumOrdW ">." '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ NumOrdW ">." '[a, a] Bool → List Term '[a, a] → [Pred] Source #
OrdLike a ⇒ Logic ">=." NumOrdW '[a, a] Bool Source #
Instance details Defined in Constrained.TheKnot Methods info ∷ NumOrdW ">=." '[a, a] Bool → String Source # propagate ∷ Context ">=." NumOrdW '[a, a] Bool hole → Specification Bool → Specification hole Source # rewriteRules ∷ NumOrdW ">=." '[a, a] Bool → List Term '[a, a] → Evidence (AppRequires ">=." NumOrdW '[a, a] Bool) → Maybe (Term Bool) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], Bool ~ b, HasSpec a0, HasSpec b) ⇒ NumOrdW ">=." '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ NumOrdW ">=." '[a, a] Bool → List Term '[a, a] → [Pred] Source #
Show (NumOrdW s ds r) Source #
Instance details Defined in Constrained.NumSpec Methods showsPrec ∷ Int → NumOrdW s ds r → ShowS show ∷ NumOrdW s ds r → String showList ∷ [NumOrdW s ds r] → ShowS
Eq (NumOrdW s ds r) Source #
Instance details Defined in Constrained.NumSpec Methods (==) ∷ NumOrdW s ds r → NumOrdW s ds r → Bool (/=) ∷ NumOrdW s ds r → NumOrdW s ds r → Bool

class (Ord a, HasSpec a) ⇒ OrdLike a where Source #

Minimal complete definition

Nothing

Methods

leqSpec ∷ a → Specification a Source #

default leqSpec ∷ (TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, OrdLike (SimpleRep a)) ⇒ a → Specification a Source #

ltSpec ∷ a → Specification a Source #

default ltSpec ∷ (TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, OrdLike (SimpleRep a)) ⇒ a → Specification a Source #

geqSpec ∷ a → Specification a Source #

default geqSpec ∷ (TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, OrdLike (SimpleRep a)) ⇒ a → Specification a Source #

gtSpec ∷ a → Specification a Source #

default gtSpec ∷ (TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, OrdLike (SimpleRep a)) ⇒ a → Specification a Source #

Instances

Instances details

(Ord a, HasSpec a, MaybeBounded a, Num a, TypeSpec a ~ NumSpec a) ⇒ OrdLike a Source #	This instance should be general enough for every type of Number that has a NumSpec as its TypeSpec
Instance details Defined in Constrained.NumSpec Methods leqSpec ∷ a → Specification a Source # ltSpec ∷ a → Specification a Source # geqSpec ∷ a → Specification a Source # gtSpec ∷ a → Specification a Source #

class MaybeBounded a where Source #

Minimal complete definition

Nothing

Methods

lowerBound ∷ Maybe a Source #

default lowerBound ∷ Bounded a ⇒ Maybe a Source #

upperBound ∷ Maybe a Source #

default upperBound ∷ Bounded a ⇒ Maybe a Source #

Instances

Instances details

MaybeBounded Int16 Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Int16 Source # upperBound ∷ Maybe Int16 Source #
MaybeBounded Int32 Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Int32 Source # upperBound ∷ Maybe Int32 Source #
MaybeBounded Int64 Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Int64 Source # upperBound ∷ Maybe Int64 Source #
MaybeBounded Int8 Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Int8 Source # upperBound ∷ Maybe Int8 Source #
MaybeBounded Word16 Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Word16 Source # upperBound ∷ Maybe Word16 Source #
MaybeBounded Word32 Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Word32 Source # upperBound ∷ Maybe Word32 Source #
MaybeBounded Word64 Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Word64 Source # upperBound ∷ Maybe Word64 Source #
MaybeBounded Word8 Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Word8 Source # upperBound ∷ Maybe Word8 Source #
MaybeBounded Integer Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Integer Source # upperBound ∷ Maybe Integer Source #
MaybeBounded Natural Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Natural Source # upperBound ∷ Maybe Natural Source #
MaybeBounded Float Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Float Source # upperBound ∷ Maybe Float Source #
MaybeBounded Int Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe Int Source # upperBound ∷ Maybe Int Source #
MaybeBounded (Ratio Integer) Source #
Instance details Defined in Constrained.NumSpec Methods lowerBound ∷ Maybe (Ratio Integer) Source # upperBound ∷ Maybe (Ratio Integer) Source #

data NumSpec n Source #

Constructors

NumSpecInterval (Maybe n) (Maybe n)

Instances

Instances details

(Arbitrary a, Ord a) ⇒ Arbitrary (NumSpec a) Source #
Instance details Defined in Constrained.NumSpec Methods arbitrary ∷ Gen (NumSpec a) Source # shrink ∷ NumSpec a → [NumSpec a] Source #
Ord n ⇒ Monoid (NumSpec n) Source #
Instance details Defined in Constrained.NumSpec Methods mempty ∷ NumSpec n mappend ∷ NumSpec n → NumSpec n → NumSpec n mconcat ∷ [NumSpec n] → NumSpec n
Ord n ⇒ Semigroup (NumSpec n) Source #
Instance details Defined in Constrained.NumSpec Methods (<>) ∷ NumSpec n → NumSpec n → NumSpec n # sconcat ∷ NonEmpty (NumSpec n) → NumSpec n stimes ∷ Integral b ⇒ b → NumSpec n → NumSpec n
Num (NumSpec Integer) Source #
Instance details Defined in Constrained.NumSpec Methods (+) ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer (-) ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer (*) ∷ NumSpec Integer → NumSpec Integer → NumSpec Integer negate ∷ NumSpec Integer → NumSpec Integer abs ∷ NumSpec Integer → NumSpec Integer signum ∷ NumSpec Integer → NumSpec Integer fromInteger ∷ Integer → NumSpec Integer
Show n ⇒ Show (NumSpec n) Source #
Instance details Defined in Constrained.NumSpec Methods showsPrec ∷ Int → NumSpec n → ShowS show ∷ NumSpec n → String showList ∷ [NumSpec n] → ShowS
Ord n ⇒ Eq (NumSpec n) Source #
Instance details Defined in Constrained.NumSpec Methods (==) ∷ NumSpec n → NumSpec n → Bool (/=) ∷ NumSpec n → NumSpec n → Bool

emptyNumSpec ∷ Ord a ⇒ NumSpec a Source #

guardNumSpec ∷ (Ord n, HasSpec n, TypeSpec n ~ NumSpec n) ⇒ [String] → NumSpec n → Specification n Source #

combineNumSpec ∷ (HasSpec n, Ord n, TypeSpec n ~ NumSpec n) ⇒ NumSpec n → NumSpec n → Specification n Source #

genFromNumSpec ∷ (MonadGenError m, Show n, Random n, Ord n, Num n, MaybeBounded n) ⇒ NumSpec n → GenT m n Source #

shrinkWithNumSpec ∷ Arbitrary n ⇒ NumSpec n → n → [n] Source #

constrainInterval ∷ (MonadGenError m, Ord a, Num a, Show a) ⇒ Maybe a → Maybe a → Integer → m (a, a) Source #

conformsToNumSpec ∷ Ord n ⇒ n → NumSpec n → Bool Source #

nubOrd ∷ Ord a ⇒ [a] → [a] Source #

Strip out duplicates (in n-log(n) time, by building an intermediate Set)

nubOrdMemberSpec ∷ Ord a ⇒ String → [a] → Specification a Source #

Builds a MemberSpec, but returns an Error spec if the list is empty

lowBound ∷ Bounded n ⇒ Maybe n → n Source #

highBound ∷ Bounded n ⇒ Maybe n → n Source #

countSpec ∷ ∀ n. (Bounded n, Integral n) ⇒ NumSpec n → Integer Source #

The exact count of the number elements in a Bounded NumSpec

finiteSize ∷ ∀ n. (Integral n, Bounded n) ⇒ Integer Source #

The exact number of elements in a Bounded Integral type.

notInNumSpec ∷ ∀ n. (HasSpec n, TypeSpec n ~ NumSpec n, Bounded n, Integral n) ⇒ NumSpec n → [n] → Specification n Source #

This is an optimizing version of TypeSpec :: TypeSpec n -> [n] -> Specification n for Bounded NumSpecs. notInNumSpec :: Bounded n => TypeSpec n -> [n] -> Specification n We use this function to specialize the (HasSpec t) method typeSpecOpt for Bounded n. So given (TypeSpec interval badlist) we might want to transform it to (MemberSpec goodlist) There are 2 opportunities where this can payoff big time. 1) Suppose the total count of the elements in the interval is < length badlist we can then return (MemberSpec (filter elements (notElem badlist))) this must be smaller than (TypeSpec interval badlist) because the filtered list must be smaller than badlist 2) Suppose the type t is finite with size N. If the length of the badlist > (N/2), then the number of possible good things must be smaller than (length badlist), because (possible good + bad == N), so regardless of the count of the interval (MemberSpec (filter elements (notElem badlist))) is better. Sometimes much better. Example, let n be the finite set {0,1,2,3,4,5,6,7,8,9} and the bad list be [0,1,3,4,5,6,8,9] (TypeSpec [0..9] [0,1,3,4,5,6,8,9]) = filter {0,1,2,3,4,5,6,7,8,9} (notElem [0,1,3,4,5,6,8,9]) = [2,7] So (MemberSpec [2,7]) is better than (TypeSpec [0..9] [0,1,3,4,5,6,8,9]). This works no matter what the count of interval is. We only need the (length badlist > (N/2)).

guardEmpty ∷ (Ord n, Num n) ⇒ Maybe n → Maybe n → NumSpec n → NumSpec n Source #

addNumSpec ∷ (Ord n, Num n) ⇒ NumSpec n → NumSpec n → NumSpec n Source #

subNumSpec ∷ (Ord n, Num n) ⇒ NumSpec n → NumSpec n → NumSpec n Source #

multNumSpec ∷ (Ord n, Num n) ⇒ NumSpec n → NumSpec n → NumSpec n Source #

negNumSpec ∷ Num n ⇒ NumSpec n → NumSpec n Source #

data T x Source #

T is a sort of special version of Maybe, with two Nothings. Given:: NumSpecInterval (Maybe n) (Maybe n) -> Numspec We can't distinguish between the two Nothings in (NumSpecInterval Nothing Nothing) But using (NumSpecInterval NegInf PosInf) we can, In fact we can make a total ordering on T So an ascending Sorted [T x] would all the NegInf on the left and all the PosInf on the right, with the Ok's sorted in between. I.e. [NegInf, NegInf, Ok 3, Ok 6, Ok 12, Pos Inf]

Constructors

NegInf
Ok x
PosInf

Instances

Instances details

Show x ⇒ Show (T x) Source #
Instance details Defined in Constrained.NumSpec Methods showsPrec ∷ Int → T x → ShowS show ∷ T x → String showList ∷ [T x] → ShowS
Ord x ⇒ Eq (T x) Source #
Instance details Defined in Constrained.NumSpec Methods (==) ∷ T x → T x → Bool (/=) ∷ T x → T x → Bool
Ord x ⇒ Ord (T x) Source #
Instance details Defined in Constrained.NumSpec Methods compare ∷ T x → T x → Ordering (<) ∷ T x → T x → Bool (<=) ∷ T x → T x → Bool (>) ∷ T x → T x → Bool (>=) ∷ T x → T x → Bool max ∷ T x → T x → T x min ∷ T x → T x → T x

unT ∷ T x → Maybe x Source #

neg ∷ Maybe x → T x Source #

Use this on the lower bound. I.e. lo from pair (lo,hi)

pos ∷ Maybe x → T x Source #

Use this on the upper bound. I.e. hi from pair (lo,hi)

multT ∷ Num x ⇒ T x → T x → T x Source #

multiply two (T x), correctly handling the infinities NegInf and PosInf

type Number n = (Num n, Enum n, TypeSpec n ~ NumSpec n, Num (NumSpec n), HasSpec n, Ord n) Source #

What constraints we need to make HasSpec instance for a Haskell numeric type. By abstracting over this, we can avoid making actual HasSpec instances until all the requirements (HasSpec Bool, HasSpec(Sum a b)) have been met in Constrained.TheKnot.

addSpecInt ∷ Number n ⇒ Specification n → Specification n → Specification n Source #

subSpecInt ∷ Number n ⇒ Specification n → Specification n → Specification n Source #

multSpecInt ∷ Number n ⇒ Specification n → Specification n → Specification n Source #

operateSpec ∷ Number n ⇒ String → (n → n → n) → (TypeSpec n → TypeSpec n → TypeSpec n) → Specification n → Specification n → Specification n Source #

let n be some numeric type, and f and ft be operations on n and (TypeSpec n) Then lift these operations from (TypeSpec n) to (Specification n) Normally f will be a (Num n) instance method (+,-,*) on n, and ft will be a a (Num (TypeSpec n)) instance method (+,-,*) on (TypeSpec n) But this will work for any operations f and ft with the right types

cardinality ∷ ∀ a. (Number Integer, HasSpec a) ⇒ Specification a → Specification Integer Source #

Put some (admittedly loose bounds) on the number of solutions that genFromTypeSpec might return. For lots of types, there is no way to be very accurate. Here we lift the HasSpec methods cardinalTrueSpec and cardinalTypeSpec from (TypeSpec Integer) to (Specification Integer)

cardinalNumSpec ∷ ∀ n. (Integral n, MaybeBounded n) ⇒ NumSpec n → Specification Integer Source #

A generic function to use as an instance for the HasSpec method cardinalTypeSpec :: HasSpec a => TypeSpec a -> Specification Integer for types n such that (TypeSpec n ~ NumSpec n)

class (Num a, HasSpec a) ⇒ NumLike a where Source #

Minimal complete definition

Nothing

Methods

subtractSpec ∷ a → TypeSpec a → Specification a Source #

default subtractSpec ∷ (TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, NumLike (SimpleRep a)) ⇒ a → TypeSpec a → Specification a Source #

negateSpec ∷ TypeSpec a → Specification a Source #

default negateSpec ∷ (TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, NumLike (SimpleRep a)) ⇒ TypeSpec a → Specification a Source #

safeSubtract ∷ a → a → Maybe a Source #

default safeSubtract ∷ (HasSimpleRep a, NumLike (SimpleRep a)) ⇒ a → a → Maybe a Source #

Instances

Instances details

Numeric a ⇒ NumLike a Source #
Instance details Defined in Constrained.NumSpec Methods subtractSpec ∷ a → TypeSpec a → Specification a Source # negateSpec ∷ TypeSpec a → Specification a Source # safeSubtract ∷ a → a → Maybe a Source #

data IntW (s ∷ Symbol) (as ∷ [Type]) b where Source #

Constructors

AddW ∷ NumLike a ⇒ IntW "addFn" '[a, a] a
NegateW ∷ NumLike a ⇒ IntW "negateFn" '[a] a

Instances

Instances details

Semantics IntW Source #
Instance details Defined in Constrained.NumSpec Methods semantics ∷ ∀ (s ∷ Symbol) (d ∷ [Type]) r. IntW s d r → FunTy d r Source #
Syntax IntW Source #
Instance details Defined in Constrained.NumSpec Methods isInFix ∷ ∀ (s ∷ Symbol) (dom ∷ [Type]) rng. IntW s dom rng → Bool Source # prettyWit ∷ ∀ (s ∷ Symbol) (dom ∷ [Type]) rng ann. (All HasSpec dom, HasSpec rng) ⇒ IntW s dom rng → List Term dom → Int → Maybe (Doc ann) Source #
NumLike a ⇒ Logic "addFn" IntW '[a, a] a Source #	Just a note that these instances won't work until we are in a context where there is a HasSpec instance of `a`, which (NumLike a) demands. This happens in Constrained.Experiment.TheKnot
Instance details Defined in Constrained.NumSpec Methods info ∷ IntW "addFn" '[a, a] a → String Source # propagate ∷ Context "addFn" IntW '[a, a] a hole → Specification a → Specification hole Source # rewriteRules ∷ IntW "addFn" '[a, a] a → List Term '[a, a] → Evidence (AppRequires "addFn" IntW '[a, a] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], a ~ b, HasSpec a0, HasSpec b) ⇒ IntW "addFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ IntW "addFn" '[a, a] Bool → List Term '[a, a] → [Pred] Source #
NumLike a ⇒ Logic "negateFn" IntW '[a] a Source #
Instance details Defined in Constrained.NumSpec Methods info ∷ IntW "negateFn" '[a] a → String Source # propagate ∷ Context "negateFn" IntW '[a] a hole → Specification a → Specification hole Source # rewriteRules ∷ IntW "negateFn" '[a] a → List Term '[a] → Evidence (AppRequires "negateFn" IntW '[a] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[a] ~ '[a0], a ~ b, HasSpec a0, HasSpec b) ⇒ IntW "negateFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ IntW "negateFn" '[a] Bool → List Term '[a] → [Pred] Source #
Show (IntW s d r) Source #
Instance details Defined in Constrained.NumSpec Methods showsPrec ∷ Int → IntW s d r → ShowS show ∷ IntW s d r → String showList ∷ [IntW s d r] → ShowS
Eq (IntW s dom rng) Source #
Instance details Defined in Constrained.NumSpec Methods (==) ∷ IntW s dom rng → IntW s dom rng → Bool (/=) ∷ IntW s dom rng → IntW s dom rng → Bool

type Numeric a = (HasSpec a, Ord a, Num a, TypeSpec a ~ NumSpec a, MaybeBounded a) Source #

addFn ∷ ∀ a. NumLike a ⇒ Term a → Term a → Term a Source #

negateFn ∷ ∀ a. NumLike a ⇒ Term a → Term a Source #

Orphan instances

Arbitrary Natural Source #
Instance details Methods arbitrary ∷ Gen Natural Source # shrink ∷ Natural → [Natural] Source #
Random Natural Source #
Instance details Methods randomR ∷ RandomGen g ⇒ (Natural, Natural) → g → (Natural, g) Source # random ∷ RandomGen g ⇒ g → (Natural, g) Source # randomRs ∷ RandomGen g ⇒ (Natural, Natural) → g → [Natural] Source # randoms ∷ RandomGen g ⇒ g → [Natural] Source #
Uniform Natural Source #
Instance details Methods uniformM ∷ StatefulGen g m ⇒ g → m Natural Source #
NumLike a ⇒ Logic "addFn" IntW '[a, a] a Source #	Just a note that these instances won't work until we are in a context where there is a HasSpec instance of `a`, which (NumLike a) demands. This happens in Constrained.Experiment.TheKnot
Instance details Methods info ∷ IntW "addFn" '[a, a] a → String Source # propagate ∷ Context "addFn" IntW '[a, a] a hole → Specification a → Specification hole Source # rewriteRules ∷ IntW "addFn" '[a, a] a → List Term '[a, a] → Evidence (AppRequires "addFn" IntW '[a, a] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[a, a] ~ '[a0], a ~ b, HasSpec a0, HasSpec b) ⇒ IntW "addFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ IntW "addFn" '[a, a] Bool → List Term '[a, a] → [Pred] Source #
NumLike a ⇒ Logic "negateFn" IntW '[a] a Source #
Instance details Methods info ∷ IntW "negateFn" '[a] a → String Source # propagate ∷ Context "negateFn" IntW '[a] a hole → Specification a → Specification hole Source # rewriteRules ∷ IntW "negateFn" '[a] a → List Term '[a] → Evidence (AppRequires "negateFn" IntW '[a] a) → Maybe (Term a) Source # mapTypeSpec ∷ ('[a] ~ '[a0], a ~ b, HasSpec a0, HasSpec b) ⇒ IntW "negateFn" '[a0] b → TypeSpec a0 → Specification b Source # saturate ∷ IntW "negateFn" '[a] Bool → List Term '[a] → [Pred] Source #
Number Integer ⇒ Num (Specification Integer) Source #	This is very liberal, since in lots of cases it returns TrueSpec. for example all operations on SuspendedSpec, and certain operations between TypeSpec and MemberSpec. Perhaps we should remove it. Only the addSpec (+) and multSpec (*) methods are used. But, it is kind of cool ... In Fact we can use this to make Num(Specification n) instance for any `n`. But, only Integer is safe, because in all other types (+) and especially (-) can lead to overflow or underflow failures.
Instance details Methods (+) ∷ Specification Integer → Specification Integer → Specification Integer (-) ∷ Specification Integer → Specification Integer → Specification Integer (*) ∷ Specification Integer → Specification Integer → Specification Integer negate ∷ Specification Integer → Specification Integer abs ∷ Specification Integer → Specification Integer signum ∷ Specification Integer → Specification Integer fromInteger ∷ Integer → Specification Integer
NumLike a ⇒ Num (Term a) Source #
Instance details Methods (+) ∷ Term a → Term a → Term a (-) ∷ Term a → Term a → Term a (*) ∷ Term a → Term a → Term a negate ∷ Term a → Term a abs ∷ Term a → Term a signum ∷ Term a → Term a fromInteger ∷ Integer → Term a
Random (Ratio Integer) Source #
Instance details Methods randomR ∷ RandomGen g ⇒ (Ratio Integer, Ratio Integer) → g → (Ratio Integer, g) Source # random ∷ RandomGen g ⇒ g → (Ratio Integer, g) Source # randomRs ∷ RandomGen g ⇒ (Ratio Integer, Ratio Integer) → g → [Ratio Integer] Source # randoms ∷ RandomGen g ⇒ g → [Ratio Integer] Source #