0 | module HTTP.API.Query
 1 |
 2 | import Data.ByteString
 3 |
 4 | %default total
 5 |
 6 | export
 7 | infix 3 ??
 8 |
 9 | ||| Mathes a single key-value pair in the *query* part of
10 | ||| the request URI.
11 | |||
12 | ||| In general, key and value are assumed to be separated by an
13 | ||| equals sign ('='), which several key-value pairs are
14 | ||| separated by an ampersand ('&').
15 | |||
16 | ||| In addition to key-value pair, boolean queries are also supported,
17 | ||| where only the presence of the key is tested, and a value can be
18 | ||| optional.
19 | public export
20 | data QField : Type where
21 |   (??)  : (name : ByteString) -> (0 type : Type) -> QField
22 |   QBool : (name : ByteString) -> QField
23 |
24 | ||| Computes the list of types captured by a URI query description.
25 | public export
26 | 0 QueryTypes : List QField -> List Type
27 | QueryTypes []               = []
28 | QueryTypes ((_ ?? t) :: xs) = t :: QueryTypes xs
29 | QueryTypes (QBool _ :: xs)  = Bool :: QueryTypes xs
30 |
31 | ||| Computes the list of types that need to be decoded from
32 | ||| a URI query part.
33 | |||
34 | ||| This is used to compute the constraints required to interpret a
35 | ||| query description.
36 | |||
37 | ||| This differs from `QueryTypes`, since boolean queries need not
38 | ||| be decoded.
39 | public export
40 | 0 QueryConstraintTypes : List QField -> List Type
41 | QueryConstraintTypes []               = []
42 | QueryConstraintTypes ((_ ?? t) :: xs) = t :: QueryConstraintTypes xs
43 | QueryConstraintTypes (QBool _ :: xs)  = QueryConstraintTypes xs
44 |
45 | ||| Wraps a list of `QField`s to account for a full description
46 | ||| of values extracted from a URI query.
47 | public export
48 | record ReqQuery where
49 |   constructor Query
50 |   fields : List QField
51 |