% $Id: URI.html,v 1.1 2003/10/01 07:22:16 connolly Exp $
Uniform Resource Identifiers (URI): Generic Syntax
(RFC 2396) T. Berners-Lee, R. Fielding, L. Masinter, August 1998
%also: RFC1630, RFC1738, RFC1808,
Web Addressing home
absoluteURI tuple of scheme: URISchemeID, path: PathName
URI_reference tuple of uri: Opt[RelAbsURI], fragment: Opt[Fragment]
URIwf tuple of abs: absoluteURI, fragment: Opt[Fragment]
combine: absoluteURI, URI_reference → URIwf
% c.f. 5.2. Resolving Relative References to Absolute Form
% combine(http://x/y, z#xyz) = http://x/z#xyz
% not defined for same-document references; i.e.
% URI_reference with null RelAbsURI
asRef: URIwf → URI_reference
% absoluteURI seen as a URI reference
wrt: URIwf, absoluteURI → URI_reference
% with respect to; i.e.
% wrt(http://x/z, http://x/y) = z
empty: → Fragment
__ # __ : absoluteURI, Fragment → URIwf
∀ i1, i2: absoluteURI, r1, r2: URI_reference,
frag: Fragment, u1, u2: URIwf
i1 # frag = [i1, value(frag)];
combine(i1, asRef(u2)) = u2;
combine(i1, wrt(u2, i1)) = u2; % @@yikes! not always true! x/../y case
% asRef is 1-1
asRef(u1) = asRef(u2) ⇒ u1=u2;
% implies ... test cases from URI spec... hmm... no, that's for
% a lower level specification.
% Issue: whether to consider URI to be the same sort as String[Char]?
% I decided not to, since I would lose a lot of sert-checking if I did.
% This doesn't mean I think URIs are something different from
% strings of characters; just that I'm keeping the fact that URIs are
% strings hidden from this specification.
% URIs are a lot like lisp symbols... in a previous revision,
% I had asString() and toURI() mappings ala lisp (print-name 'sym).
% But for this level of specification, I don't need to decide
% that URIs are strings nor decide that they're different from strings.
% The URISyntax trait knows they're the same.
% Similarly for PortNum, DomainName, etc. These represent things
% that denote ports and domains, not the ports and domains themselves.
HTML generated using lsl2html.