0 | module TyTTP.HTTP.Consumer
2 | import Control.Monad.Trans
3 | import Control.Monad.Either
6 | import public Data.List.Quantifiers
11 | import TyTTP.HTTP.Protocol
14 | interface Accept t where
15 | contentType : (ty : Type) -> { auto p : ty = t } -> List String
18 | data IsAccept : (t : Type) -> Type where
19 | ItIsAccept : Accept t => IsAccept t
22 | ConsumerError : Type
23 | ConsumerError = String
26 | interface Accept t => Consumer a t where
27 | consumeRaw : (ty : Type) -> { auto p : ty = t } -> (ct : String) -> (raw : Buffer) -> Either ConsumerError a
30 | data IsConsumer : (a : Type) -> (t : Type) -> Type where
31 | ItIsConsumer : Consumer a t => IsConsumer a t
36 | unsafeConsumeBody : Error e
38 | => MonadPromise e m p
40 | Context me u v h1 s h2 Buffer b
41 | -> (forall p'. MonadPromise e m p' => p' $
Context me' u' v' h1' s' h2' a' b')
43 | -> Context me u v h1 s h2 (Publisher m e Buffer) b
44 | -> p $
Context me' u' v' h1' s' h2' a' b'
45 | unsafeConsumeBody handler ctx = promise $
\resolve', reject' => do
47 | let subscriber : Subscriber m e Buffer = MkSubscriber
48 | { onNext = \a => modifyIORef acc (:< a)
49 | , onSucceded = \_ => do
50 | all <- concatBuffers =<< asList <$> readIORef acc
51 | Just emptyBuffer <- newBuffer 0 | _ => assert_total $
idris_crash "creating an empty buffer has failed"
52 | let result = handler $
{ request.body := fromMaybe emptyBuffer all } ctx
53 | runPromise { m = m } resolve' reject' result
54 | , onFailed = reject'
56 | ctx.request.body.subscribe subscriber
60 | -> (isConsumer : IsConsumer a t)
63 | -> Either ConsumerError a
64 | consumePayload t ItIsConsumer ct raw =
70 | => MonadPromise e IO m
71 | => Alternative (t m)
72 | => HasContentType h1
73 | => (list: List Type)
74 | -> (areAccepts : All IsAccept list)
75 | -> (areConsumers : All (IsConsumer a) list)
78 | Context me u v h1 s h2 (Either ConsumerError a) b
79 | -> (forall m'. MonadPromise e IO m' => m' $
Context me' u' v' h1' s' h2' a' b')
81 | -> Context me u v h1 s h2 (Publisher IO e Buffer) b
82 | -> t m $
Context me' u' v' h1' s' h2' (Publisher IO e Buffer) b'
83 | safeConsume [] _ _ _ _ _ = empty
84 | safeConsume (t::ts) (ItIsAccept::as) (c::cs) ct handler ctx =
85 | if elem ct (contentType t)
86 | then lift $
flip unsafeConsumeBody ctx $
\ctx' => promise $
\resolve' ,reject' => do
87 | let raw = ctx'.request.body
88 | result = handler $
{ request.body := consumePayload t c ct raw } ctx'
89 | success = \r => resolve' $
{ request.body := singleton raw } r
90 | runPromise { m = IO } success reject' result
91 | else safeConsume ts as cs ct handler ctx
97 | => MonadPromise e IO m
98 | => Alternative (t m)
99 | => HasContentType h1
100 | => (list: List Type)
101 | -> {auto isNonEmpty : NonEmpty list}
102 | -> {auto areAccepts : All IsAccept list}
103 | -> {auto areConsumers : All (IsConsumer a) list}
105 | Context me u v h1 s h2 (Either ConsumerError a) b
106 | -> (forall m'. MonadPromise e IO m' => m' $
Context me' u' v' h1' s' h2' a' b')
108 | -> Context me u v h1 s h2 (Publisher IO e Buffer) b
109 | -> t m $
Context me' u' v' h1' s' h2' (Publisher IO e Buffer) b'
110 | consumes list {isNonEmpty} {areAccepts} {areConsumers} handler ctx = do
111 | let Just ct = getContentType ctx.request.headers
114 | safeConsume list areAccepts areConsumers ct handler ctx
120 | => MonadPromise e IO m
121 | => Alternative (t m)
122 | => HasContentType h1
123 | => (list: List Type)
124 | -> {auto isNonEmpty : NonEmpty list}
125 | -> {auto areAccepts : All IsAccept list}
126 | -> {auto areConsumers : All (IsConsumer a) list}
128 | Context me u v h1 s h2 ConsumerError b
129 | -> (forall m'. MonadPromise e IO m' => m' $
Context me' u' v' h1' s' h2' a' b')
132 | Context me u v h1 s h2 a b
133 | -> (forall m''. MonadPromise e IO m'' => m'' $
Context me' u' v' h1' s' h2' a'' b')
135 | -> Context me u v h1 s h2 (Publisher IO e Buffer) b
136 | -> t m $
Context me' u' v' h1' s' h2' (Publisher IO e Buffer) b'
137 | consumes' list {isNonEmpty} {areAccepts} {areConsumers} errHandler handler ctx =
139 | Context me u v h1 s h2 (Either ConsumerError a) b
140 | -> (forall m'. MonadPromise e IO m' => m' $
Context me' u' v' h1' s' h2' () b')
142 | case s.request.body of
144 | result <- handler $
{ request.body := r } s
145 | pure $
{ request.body := () } result
147 | result <- errHandler $
{ request.body := l } s
148 | pure $
{ request.body := () } result
149 | in consumes list handler' ctx