0 | module HTTP.Header.Types
 1 |
 2 | import Data.ByteString
 3 | import Data.SortedMap
 4 | import Derive.Prelude
 5 |
 6 | %default total
 7 | %language ElabReflection
 8 |
 9 | public export
10 | data Parameter : Type where
11 |   P : (name, value : String) -> Parameter
12 |   Q : Double -> Parameter
13 |
14 | %runElab derive "Parameter" [Show,Eq]
15 |
16 | public export
17 | 0 Parameters : Type
18 | Parameters = List Parameter
19 |
20 | export
21 | parameter : String -> Parameters -> Maybe String
22 | parameter s (P n v :: xs) = if s == n then Just v else parameter s xs
23 | parameter s _             = Nothing
24 |
25 | export
26 | weight : Parameters -> Double
27 | weight (Q v   :: xs) = v
28 | weight (P _ _ :: xs) = weight xs
29 | weight []            = 1.0
30 |
31 | public export
32 | data MediaDesc : Type where
33 |   MDAny  : MediaDesc
34 |   MDStar : (type : String) -> MediaDesc
35 |   MD     : (type, subtype : String) -> MediaDesc
36 |
37 | %runElab derive "MediaDesc" [Show,Eq]
38 |
39 | public export
40 | record MediaRange where
41 |   constructor MR
42 |   type   : MediaDesc
43 |   params : Parameters
44 |
45 | %runElab derive "MediaRange" [Show,Eq]
46 |
47 | public export
48 | record MediaType where
49 |   constructor MT
50 |   type    : String
51 |   subtype : String
52 |
53 | export
54 | encodeMediaType : MediaType -> ByteString
55 | encodeMediaType (MT t s) = fromString "\{t}/\{s}"
56 |
57 | %runElab derive "MediaType" [Show,Eq]
58 |
59 | public export
60 | record ContentType where
61 |   constructor CT
62 |   type   : MediaType
63 |   params : Parameters
64 |
65 | %runElab derive "ContentType" [Show,Eq]
66 |
67 | export
68 | accepts : MediaDesc -> MediaType -> Bool
69 | accepts MDAny             _ = True
70 | accepts (MDStar type)     t = type == t.type
71 | accepts (MD type subtype) t = type == t.type && subtype == t.subtype
72 |
73 | public export
74 | 0 MediaRanges : Type
75 | MediaRanges = List MediaRange
76 |
77 | public export
78 | record ContentDisp where
79 |   constructor CD
80 |   disp   : String
81 |   params : Parameters
82 |
83 | %runElab derive "ContentDisp" [Show,Eq]
84 |
85 | public export
86 | 0 HeaderMap : Type
87 | HeaderMap = SortedMap String ByteString
88 |