Control.Validation

Definitions

Result : (Type -> Type) -> Type -> Type

Totality: total
Visibility: public export

data ValidatorT : (Type -> Type) -> Type -> Type -> Type

  Validators in this module come in two flavours: Structural Validators and
  Property Validators. They are both wrappers around functions which take
  some input and confirm that it's valid (returning some witness of its
  validity) or fail with an error described by a string.

Totality: total
Visibility: export
Constructor: 

MkValidator : (a -> Result m b) -> ValidatorT m a b

Hints:

Monad m => Alternative (ValidatorT m a)

Monad m => Applicative (ValidatorT m a)

Functor m => Functor (ValidatorT m a)

Monad m => Monad (ValidatorT m a)

Validator : Type -> Type -> Type

Totality: total
Visibility: public export

validateT : ValidatorT m a b -> a -> Result m b

  Run validation on given input, returning (Right refinedInput) if everything
  is all right or (Left errorMessage) if it's not.

Totality: total
Visibility: export

validate : Validator a b -> a -> Either String b

  Run validation within the Identity monad and unwrap result immediately.

Totality: total
Visibility: export

validator : (a -> Result m b) -> ValidatorT m a b

  Given a function from input to Either String output, make a validator.

Totality: total
Visibility: export

withError : Monad m => String -> ValidatorT m a b -> ValidatorT m a b

  Replace validator's default error message.

Totality: total
Visibility: export

fail : Applicative m => String -> ValidatorT m a b

  A validator which always fails with a given message.

Totality: total
Visibility: export

(>>>) : Monad m => ValidatorT m a b -> ValidatorT m b c -> ValidatorT m a c

  Compose two validators so that the second validates the output of the first.

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 2

contramap : (a -> b) -> ValidatorT m b c -> ValidatorT m a c

  Alter the input before validation using given function.

Totality: total
Visibility: export

decide : Monad m => (t -> String) -> ((x : t) -> Dec (p x)) -> PropValidator m t p

  Given a value x and a decision procedure for property p, validateT if p x
  holds, returning a proof if it does. The procedure also has access to the
  raw input in case it was helpful.

Totality: total
Visibility: export

fromMaybe : Monad m => (a -> String) -> (a -> Maybe b) -> ValidatorT m a b

  Given a function converting a into Maybe b, build a Validator of a
  converting it into b.

Totality: total
Visibility: export

natural : Monad m => ValidatorT m String Nat

  Verify whether a String represents a natural number.

Totality: total
Visibility: export

integral : Num a => Neg a => Monad m => ValidatorT m String a

  Verify whether a String represents an Integer

Totality: total
Visibility: export

double : Monad m => ValidatorT m String Double

  Verify that a string represents a decimal fraction.

Totality: total
Visibility: export

length : Monad m => (l : Nat) -> ValidatorT m (List a) (Vect l a)

  Verify whether a list has a desired length.

Totality: total
Visibility: export

equal : Monad m => DecEq t => (a : t) -> PropValidator m t (\b => a = b)

  Verify that certain values are equal.

Totality: total
Visibility: export

lteNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip LTE bound)

  Verify that a Nat is less than or equal to  certain bound.

Totality: total
Visibility: export

gteNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip GTE bound)

  Verify that a Nat is greater than or equal to certain bound.

Totality: total
Visibility: export

ltNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip LT bound)

  Verify that a Nat is strictly less than a certain bound.

Totality: total
Visibility: export

gtNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip GT bound)

  Verify that a Nat is strictly greate than a certain bound.

Totality: total
Visibility: export