Data.URI

Module for parsing and handling of URIs.

References:
  [1] https://tools.ietf.org/html/rfc3986
  [2] https://tools.ietf.org/html/rfc6874
  [3] https://tools.ietf.org/html/rfc7320
  [4] https://tools.ietf.org/html/rfc8820

(C) The Idris Community, 2021

Definitions

record URIAuthority : Type

  Type of an authority within URIs.

Totality: total
Visibility: public export
Constructor: 

MkURIAuthority : Maybe String -> String -> Maybe Nat -> URIAuthority

Projections:

.port : URIAuthority -> Maybe Nat

.regName : URIAuthority -> String

.userInfo : URIAuthority -> Maybe String

Hints:

Eq URIAuthority

Ord URIAuthority

Show URIAuthority

.userInfo : URIAuthority -> Maybe String

Visibility: public export

userInfo : URIAuthority -> Maybe String

Visibility: public export

.regName : URIAuthority -> String

Visibility: public export

regName : URIAuthority -> String

Visibility: public export

.port : URIAuthority -> Maybe Nat

Visibility: public export

port : URIAuthority -> Maybe Nat

Visibility: public export

record URI : Type

  Type for a general URI.

Totality: total
Visibility: public export
Constructor: 

MkURI : String -> Maybe URIAuthority -> String -> String -> String -> URI

Projections:

.authority : URI -> Maybe URIAuthority

.fragment : URI -> String

.path : URI -> String

.query : URI -> String

.scheme : URI -> String

Hints:

Eq URI

Ord URI

Show URI

.scheme : URI -> String

Visibility: public export

scheme : URI -> String

Visibility: public export

.authority : URI -> Maybe URIAuthority

Visibility: public export

authority : URI -> Maybe URIAuthority

Visibility: public export

.path : URI -> String

Visibility: public export

path : URI -> String

Visibility: public export

.query : URI -> String

Visibility: public export

query : URI -> String

Visibility: public export

.fragment : URI -> String

Visibility: public export

fragment : URI -> String

Visibility: public export

uriParser : Parser URI

  Parser for a generic URI.
  
  @see RFC 3986, section 3

Visibility: export

uriReferenceParser : Parser URI

  Parser for a URI reference.
  
  @see RFC 3986, section 4.1

Visibility: export

uriAbsoluteParser : Parser URI

  Parser for an absolute URI without a fragment identifier.
  
  @see RFC 3986, section 4.3

Visibility: export

uriIsAbsolute : URI -> Bool

Visibility: export

uriIsRelative : URI -> Bool

Visibility: export

isUnescapedInURI : Char -> Bool

Visibility: export

isUnescapedInURIComponent : Char -> Bool

Visibility: export

escapeURIChar : (Char -> Bool) -> Char -> String

Visibility: export

escapeURIString : (Char -> Bool) -> String -> String

Visibility: export

escapeAndParseURI : String -> Either String URI

Visibility: export