0 | module Control.Validation
  1 |
  2 | -- Main purpose of this module is verifying programmer's assumptions about
  3 | -- user input. On one hand we want to write precisely typed programs, including
  4 | -- assumptions about input expressed in types and prove correctness of these
  5 | -- programs. On the other we get an unstructured user input as a string or even
  6 | -- a raw sequence of bytes.
  7 |
  8 | -- This module intends to provide a framework for verifying our assumptions
  9 | -- about user input and constructing proofs that input is indeed valid or
 10 | -- failing early with a nice error message if it isn't.
 11 |
 12 | import Control.Monad.Identity
 13 | import Control.Monad.Error.Either
 14 | import Data.Nat
 15 | import Data.String
 16 | import Data.Vect
 17 | import Decidable.Equality
 18 |
 19 | %default total
 20 |
 21 |
 22 | public export
 23 | Result : (Type -> Type) -> Type -> Type
 24 | Result m = EitherT String m
 25 |
 26 | ||| Validators in this module come in two flavours: Structural Validators and
 27 | ||| Property Validators. They are both wrappers around functions which take
 28 | ||| some input and confirm that it's valid (returning some witness of its
 29 | ||| validity) or fail with an error described by a string.
 30 | export
 31 | data ValidatorT : (Type -> Type) -> Type -> Type -> Type where
 32 |     MkValidator : (a -> Result m b) -> ValidatorT m a b
 33 |
 34 | ||| A type of validator trying to prove properties of values. It's type is
 35 | ||| significantly different than that of an ordinary validator and cannot be
 36 | ||| made an instance of Monad interface, because it's last parameter is
 37 | ||| (t -> Type) instead of just Type. Therefore it must be explicitly turned
 38 | ||| into an ordinary validator using the prop function below.
 39 | data PropValidator : (Type -> Type) -> (t : Type) -> (t -> Type) -> Type where
 40 |     MkPropValidator : ((x : t) -> Result m (p x)) -> PropValidator m t p
 41 |
 42 | public export
 43 | Validator : Type -> Type -> Type
 44 | Validator = ValidatorT Identity
 45 |
 46 |
 47 | ||| Run validation on given input, returning (Right refinedInput) if everything
 48 | ||| is all right or (Left errorMessage) if it's not.
 49 | export
 50 | validateT : ValidatorT m a b -> a -> Result m b
 51 | validateT (MkValidator v) = v
 52 |
 53 | ||| Run validation within the Identity monad and unwrap result immediately.
 54 | export
 55 | validate : Validator a b -> a -> Either String b
 56 | validate v = runIdentity . runEitherT . validateT v
 57 |
 58 | ||| Given a function from input to Either String output, make a validator.
 59 | export
 60 | validator : (a -> Result m b) -> ValidatorT m a b
 61 | validator = MkValidator
 62 |
 63 | export
 64 | Functor m => Functor (ValidatorT m a) where
 65 |     map f v = MkValidator (map f . validateT v)
 66 |
 67 | export
 68 | Monad m => Applicative (ValidatorT m a) where
 69 |     pure a = MkValidator (const $ pure a)
 70 |     f <*> a = MkValidator (\x => validateT f x <*> validateT a x)
 71 |
 72 | export
 73 | Monad m => Monad (ValidatorT m a) where
 74 |     v >>= f = MkValidator $ \x => do
 75 |         r <- validateT v x
 76 |         validateT (f r) x
 77 |
 78 | ||| Plug a property validator into the chain of other validators. The value
 79 | ||| under validation will be ignored and the value whose property is going to
 80 | ||| be checked must be supplied manually. Otherwise Idris won;t be able to
 81 | ||| unify.
 82 | prop : PropValidator m t p -> (x : t) -> ValidatorT m a (p x)
 83 | prop (MkPropValidator v) x = MkValidator (const $ v x)
 84 |
 85 | replaceError : Monad m => String -> Result m a -> Result m a
 86 | replaceError e = bimapEitherT (const e) id
 87 |
 88 | ||| Replace validator's default error message.
 89 | export
 90 | withError : Monad m => String -> ValidatorT m a b -> ValidatorT m a b
 91 | withError e (MkValidator f) = MkValidator (replaceError e . f)
 92 |
 93 | ||| A validator which always fails with a given message.
 94 | export
 95 | fail : Applicative m => String -> ValidatorT m a b
 96 | fail s = MkValidator $ \_ => left s
 97 |
 98 | export infixl 2 >>>
 99 |
100 | ||| Compose two validators so that the second validates the output of the first.
101 | export
102 | (>>>) : Monad m => ValidatorT m a b -> ValidatorT m b c -> ValidatorT m a c
103 | left >>> right = MkValidator (validateT left >=> validateT right)
104 |
105 | Monad m => Alternative (ValidatorT m a) where
106 |     left <|> right = MkValidator $ \x => MkEitherT $ do
107 |         case !(runEitherT $ validateT left x) of
108 |             (Right r) => pure $ Right r
109 |             (Left e) => case !(runEitherT $ validateT right x) of
110 |                 (Right r) => pure $ Right r
111 |                 (Left e') => pure $ Left (e <+> " / " <+> e')
112 |
113 |     empty = MkValidator $ \x => MkEitherT $ pure (Left "invalid")
114 |
115 | ||| Alter the input before validation using given function.
116 | export
117 | contramap : (a -> b) -> ValidatorT m b c -> ValidatorT m a c
118 | contramap f v = MkValidator (validateT v . f)
119 |
120 |
121 | ||| Given a value x and a decision procedure for property p, validateT if p x
122 | ||| holds, returning a proof if it does. The procedure also has access to the
123 | ||| raw input in case it was helpful.
124 | export
125 | decide : Monad m => (t -> String) -> ((x : t) -> Dec (p x)) -> PropValidator m t p
126 | decide msg dec = MkPropValidator $ \x => case dec x of
127 |     Yes prf => pure prf
128 |     No _ => left (msg x)
129 |
130 | ||| Given a function converting a into Maybe b, build a Validator of a
131 | ||| converting it into b.
132 | export
133 | fromMaybe : Monad m => (a -> String) -> (a -> Maybe b) -> ValidatorT m a b
134 | fromMaybe e f = MkValidator $ \a => case f a of
135 |     Nothing => left $ e a
136 |     Just b => pure b
137 |
138 | ||| Verify whether a String represents a natural number.
139 | export
140 | natural : Monad m => ValidatorT m String Nat
141 | natural = fromMaybe mkError parsePositive
142 |     where
143 |     mkError : String -> String
144 |     mkError s = "'" <+> s <+> "' is not a natural number."
145 |
146 | ||| Verify whether a String represents an Integer
147 | export
148 | integral : Num a => Neg a => Monad m => ValidatorT m String a
149 | integral = fromMaybe mkError parseInteger
150 |     where
151 |     mkError : String -> String
152 |     mkError s = "'" <+> s <+> "' is not an integer."
153 |
154 | ||| Verify that a string represents a decimal fraction.
155 | export
156 | double : Monad m => ValidatorT m String Double
157 | double = fromMaybe mkError parseDouble
158 |     where
159 |     mkError : String -> String
160 |     mkError s = "'" <+> s <+> "is not a decimal."
161 |
162 |
163 | ||| Verify whether a list has a desired length.
164 | export
165 | length : Monad m => (l : Nat) -> ValidatorT m (List a) (Vect l a)
166 | length l = MkValidator (validateVector l)
167 |     where
168 |     validateVector : (l : Nat) -> List a -> Result m (Vect l a)
169 |     validateVector Z [] = pure []
170 |     validateVector (S _) [] = left "Missing list element."
171 |     validateVector Z (_ :: _) = left "Excessive list element."
172 |     validateVector (S k) (x :: xs) = do
173 |         ys <- validateVector k xs
174 |         pure (x :: ys)
175 |
176 | ||| Verify that certain values are equal.
177 | export
178 | equal : Monad m => DecEq t => (a : t) -> PropValidator m t (\b => a = b)
179 | equal a = MkPropValidator $ \b => case decEq a b of
180 |     Yes prf => pure prf
181 |     No _ => left "Values are not equal."
182 |
183 | ||| Verify that a Nat is less than or equal to  certain bound.
184 | export
185 | lteNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip LTE bound)
186 | lteNat bound = decide
187 |     (\n => show n <+> " is not lower or equal to " <+> show bound)
188 |     (\n => isLTE n bound)
189 |
190 | ||| Verify that a Nat is greater than or equal to certain bound.
191 | export
192 | gteNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip GTE bound)
193 | gteNat bound = decide
194 |     (\n => show n <+> " is not greater or equal to " <+> show bound)
195 |     (isLTE bound)
196 |
197 | ||| Verify that a Nat is strictly less than a certain bound.
198 | export
199 | ltNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip LT bound)
200 | ltNat bound = decide
201 |     (\n => show n <+> " is not strictly lower than " <+> show bound)
202 |     (\n => isLTE (S n) bound)
203 |
204 | ||| Verify that a Nat is strictly greater than a certain bound.
205 | export
206 | gtNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip GT bound)
207 | gtNat bound = decide
208 |     (\n => show n <+> " is not strictly greater than " <+> show bound)
209 |     (isLTE (S bound))
210 |