Hedgehog.Internal.Range

Definitions

MaxSizeNat : Nat

Totality: total
Visibility: public export

record Size : Type

  A wrapper of a natural number plus an erased proof that
  the value is within its bounds.
  
  Unlike the original Hedgehog, we allow values in the range [0,100]
  treating size as a proper percentage.

Totality: total
Visibility: public export
Constructor: 

MkSize : (size : Nat) -> (0 _ : size <= MaxSizeNat = True) -> Size

Projections:

.size : Size -> Nat

0 .sizeOk : ({rec:0} : Size) -> size {rec:0} <= MaxSizeNat = True

Hints:

Eq Size

MaxBound Size

MinBound Size

Num Size

Ord Size

Pretty Size

Show Size

ToInteger Size

.size : Size -> Nat

Totality: total
Visibility: public export

size : Size -> Nat

Totality: total
Visibility: public export

0 .sizeOk : ({rec:0} : Size) -> size {rec:0} <= MaxSizeNat = True

Totality: total
Visibility: public export

0 sizeOk : ({rec:0} : Size) -> size {rec:0} <= MaxSizeNat = True

Totality: total
Visibility: public export

mkSize : (n : Nat) -> {auto 0 _ : n <= MaxSizeNat = True} -> Size

Totality: total
Visibility: public export

minSize : Size

Totality: total
Visibility: public export

maxSize : Size

Totality: total
Visibility: public export

mkSizeMay : Nat -> Maybe Size

Totality: total
Visibility: export

mkSizeOrZero : Nat -> Size

Totality: total
Visibility: export

mkSizeOrMax : Nat -> Size

Totality: total
Visibility: export

resize : (Nat -> Nat) -> Size -> Size

Totality: total
Visibility: public export

record Range : Type -> Type

Totality: total
Visibility: public export
Constructor: 

MkRange : a -> (Size -> (a, a)) -> Range a

Projections:

.bounds' : Range a -> Size -> (a, a)

.origin : Range a -> a

Hint: 

Functor Range

.origin : Range a -> a

Totality: total
Visibility: public export

origin : Range a -> a

Totality: total
Visibility: public export

.bounds' : Range a -> Size -> (a, a)

Totality: total
Visibility: public export

bounds' : Range a -> Size -> (a, a)

Totality: total
Visibility: public export

bounds : Size -> Range a -> (a, a)

Totality: total
Visibility: export

lowerBound : Ord a => Size -> Range a -> a

  Get the lower bound of a range for the given size.

Totality: total
Visibility: export

upperBound : Ord a => Size -> Range a -> a

  Get the lower bound of a range for the given size.

Totality: total
Visibility: export

singleton : a -> Range a

  Construct a range which represents a constant single value.
  
  >>> bounds x $ singleton 5
  (5,5)
  
  >>> origin $ singleton 5
  5

Totality: total
Visibility: export

constantFrom : a -> a -> a -> Range a

  Construct a range which is unaffected by the size parameter with a origin
  point which may differ from the bounds.
  
  A range from @-10@ to @10@, with the origin at @0@:
  
  >>> bounds x $ constantFrom 0 (-10) 10
  (-10,10)
  
  >>> origin $ constantFrom 0 (-10) 10
  0
  
  A range from @1970@ to @2100@, with the origin at @2000@:
  
  >>> bounds x $ constantFrom 2000 1970 2100
  (1970,2100)
  
  >>> origin $ constantFrom 2000 1970 2100
  2000

Totality: total
Visibility: export

constant : a -> a -> Range a

  Construct a range which is unaffected by the size parameter.
  
  A range from @0@ to @10@, with the origin at @0@:
  
  >>> bounds x $ constant 0 10
  (0,10)
  
  >>> origin $ constant 0 10
  0
  

Totality: total
Visibility: export

constantBounded : (MinBound a, MaxBound a) => Num a => Range a

  Construct a range which is unaffected by the size parameter using the full
  range of a data type.
  
  A range from @-128@ to @127@, with the origin at @0@:
  
  >>> bounds x (constantBounded :: Range Int8)
  (-128,127)
  
  >>> origin (constantBounded :: Range Int8)
  0

Totality: total
Visibility: export

clamp : Ord a => a -> a -> a -> a

  Truncate a value so it stays within some range.
  
  >>> clamp 5 10 15
  10
  
  >>> clamp 5 10 0
  5

Totality: total
Visibility: export

scaleLinear : ToInteger a => Size -> a -> a -> a

  Scales an integral value linearly with the size parameter.

Totality: total
Visibility: export

scaleLinearFrac : Fractional a => Neg a => Size -> a -> a -> a

  Scales a fractional value linearly with the size parameter.

Totality: total
Visibility: export

scaled : Ord a => (Size -> a -> a -> a) -> a -> a -> a -> Range a

Totality: total
Visibility: export

linearFrom : Ord a => ToInteger a => a -> a -> a -> Range a

  Construct a range which scales the bounds relative to the size parameter.
  
  >>> bounds 0 $ linearFrom 0 (-10) 10
  (0,0)
  
  >>> bounds 50 $ linearFrom 0 (-10) 20
  (-5,10)
  
  >>> bounds 100 $ linearFrom 0 (-10) 20
  (-10,20)

Totality: total
Visibility: export

linear : Ord a => ToInteger a => a -> a -> Range a

Totality: total
Visibility: export

linearFin : (n : Nat) -> Range (Fin (S n))

Totality: total
Visibility: export

linearFracFrom : Ord a => Fractional a => Neg a => a -> a -> a -> Range a

  Construct a range which scales the bounds relative to the size parameter.
  
  This works the same as 'linearFrom', but for fractional values.

Totality: total
Visibility: export

linearBounded : (MinBound a, MaxBound a) => Ord a => ToInteger a => Range a

  Construct a range which is scaled relative to the size parameter and uses
  the full range of a data type.
  
  >>> bounds 0 (linearBounded :: Range Int8)
  (0,0)
  
  >>> bounds 50 (linearBounded :: Range Int8)
  (-64,64)
  
  >>> bounds 99 (linearBounded :: Range Int8)
    (-128,127)

Totality: total
Visibility: export

scaleExponentialDouble : Size -> Double -> Double -> Double

  Scale a floating-point number exponentially with the size parameter.
  
  Note : This scales the difference between the two values exponentially.

Totality: total
Visibility: export

scaleExponential : ToInteger a => Size -> a -> a -> a

  Scale an integral exponentially with the size parameter.

Totality: total
Visibility: export

exponentialDoubleFrom : Double -> Double -> Double -> Range Double

Totality: total
Visibility: export

exponentialDouble : Double -> Double -> Range Double

Totality: total
Visibility: export

exponentialFrom : Ord a => ToInteger a => a -> a -> a -> Range a

Totality: total
Visibility: export

exponential : Ord a => ToInteger a => a -> a -> Range a

Totality: total
Visibility: export

exponentialFin : (n : Nat) -> Range (Fin (S n))

Totality: total
Visibility: export