URI

% $Id: URI.html,v 1.1 2003/10/01 07:22:16 connolly Exp $

References

Uniform Resource Identifiers (URI): Generic Syntax
(RFC 2396) T. Berners-Lee, R. Fielding, L. Masinter, August 1998
%also: RFC1630, RFC1738, RFC1808,
Web Addressing home

URI: trait
   includes
      NullOpt(RelAbsURI),
      NullOpt(Fragment)

   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]

   introduces

      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

   asserts

     ∀ 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.

[Index]

HTML generated using lsl2html.