
  0 | module HTTP.URI
  1 | 
  2 | import Data.Buffer
  3 | import Derive.Prelude
  4 | import HTTP.Parser.URI
  5 | import HTTP.Parser.Util
  6 | import Text.ILex
  7 | 
  8 | %hide Data.Linear.(.)
  9 | %default total
 10 | %language ElabReflection
 11 | 
 12 | public export
 13 | data QueryVal : Type where
 14 |   QVal   : (v : ByteString) -> QueryVal
 15 |   QEmpty : QueryVal
 16 | 
 17 | %runElab derive "QueryVal" [Show,Eq]
 18 | 
 19 | public export
 20 | 0 Queries : Type
 21 | Queries = List (ByteString,QueryVal)
 22 | 
 23 | ||| -- TODO: Special treatment of user info
 24 | public export
 25 | record URI where
 26 |   constructor MkURI
 27 |   scheme    : Maybe ByteString
 28 |   authority : Maybe ByteString
 29 |   abs       : Bool
 30 |   path      : List ByteString
 31 |   queries   : Queries
 32 |   fragment  : Maybe ByteString
 33 | 
 34 | %runElab derive "URI" [Show,Eq]
 35 | 
 36 | toQueries : ByteString -> Queries
 37 | toQueries = map qpair . split byte_ampersand
 38 |   where
 39 |     qpair : ByteString -> (ByteString, QueryVal)
 40 |     qpair bs =
 41 |       case break (byte_equals ==) bs of
 42 |         (pre, BS (S k) bv) => (pre, QVal $ BS k $ tail bv)
 43 |         (pre, _)           => (pre, QEmpty)
 44 | 
 45 | encodeQueries : Queries -> List ByteString
 46 | encodeQueries [] = []
 47 | encodeQueries ps = "?" :: intersperse "&" (map qpair ps)
 48 |   where
 49 |     qpair : (ByteString, QueryVal) -> ByteString
 50 |     qpair (n, v) =
 51 |      let en := uriEscape (not . isQueryNameByte) n
 52 |       in case v of
 53 |            QEmpty => en
 54 |            QVal x => fastConcat [en,"=",uriEscape (not . isQueryByte) x]
 55 | 
 56 | toURI : Part -> URI
 57 | toURI (P sch auth abs segs ques frag) =
 58 |   MkURI sch auth abs (segs <>> []) (maybe empty toQueries ques) frag
 59 | 
 60 | pathLines : URI -> List ByteString
 61 | pathLines (MkURI s a abs p q f) =
 62 |      (if abs || not (null a || null p) then ["/"] else [])
 63 |   ++ intersperse "/" (map (uriEscape (not . ispchar)) p)
 64 | 
 65 | export %inline
 66 | encodePath : URI -> ByteString
 67 | encodePath = fastConcat . pathLines
 68 | 
 69 | ||| Properly escapes characters in a URL if necessary and
 70 | ||| combines the different parts in the URI.
 71 | export
 72 | encodeURI : URI -> ByteString
 73 | encodeURI u@(MkURI s a _ _ q f) =
 74 |   fastConcat $
 75 |        maybe [] (::[":"]) s
 76 |     ++ maybe [] (\x => ["//", uriEscape (not . isAuthByte) x]) a
 77 |     ++ pathLines u
 78 |     ++ encodeQueries q
 79 |     ++ maybe [] (\x => ["#", uriEscape (not . isFragmentByte) x]) f
 80 | 
 81 | export %inline
 82 | parseURI : Origin -> ByteString -> Either (ParseError Void) URI
 83 | parseURI o = map toURI . parseBytes uri o
 84 | 
 85 | export %inline
 86 | Interpolation URI where
 87 |   interpolate = toString . encodeURI
 88 | 
 89 | --------------------------------------------------------------------------------
 90 | -- Test Parsing
 91 | --------------------------------------------------------------------------------
 92 | 
 93 | export
 94 | testParseURI : ByteString -> IO ()
 95 | testParseURI =
 96 |   either (putStrLn . interpolate) (putStrLn . interpolate) . parseURI Virtual
 97 |