% $Id: URIclient.lsl,v 1.1 2001/01/31 07:39:53 connolly Exp $
%
% cf first figure of
% Univeral Resource Identifiers -- Axioms of Web architecture
% http://www.w3.org/DesignIssues/Model
% http://www.w3.org/DesignIssues/ParseHash.png
%
% Uniform Resource Identifiers (URI): Generic Syntax
% August 1998
% http://www.ietf.org/rfc/rfc2396.txt

URIclient: trait
  includes Integer, String(Char)
  
  introduces
    % charmod spec
    US_ASCII : -> CodedCharacterSet
    __ [ __ ] : CodedCharacterSet, Int -> Char

    asString: URI -> String[Char] % @@what's this called in the IMoniker docs?
    asString: Atom -> String[Char]

    __ # __ : Path, Atom -> URI  % "foo#bar"
    asURI: Path -> URI           % "foo"

    % section @@ self document reference
    self: -> Path                % ""
    self: -> URI                 % ""
    parent: Path -> Path         % parent("foo") = "../foo"
    root1: Path -> Path          % root1("foo") -> "/foo"
    absolute: URI -> Bool        % foo:bar vs. foo
                                 % @@ax: includes colon /\ stuff before colon is an atom

    hash, colon, slash, ques: -> Char

    corefer: URI, URI, URI -> Bool
    % for corefer(this, that, there) read: _this_ URI in this
    % document refers to the same thing/resource as _that_ URI
    % in a document whose address is _there_ from this document.

  asserts
    forall this, that, there: URI, p, p1, p2, p3: Path, a: Atom, c: Char

      hash = US_ASCII[35];
      colon = US_ASCII[58];
      ques = US_ASCII[63];
      slash = US_ASCII[47];

      (asString(this) = asString(that)) => this=that;

      asString(self) = empty;
      self = asURI(self);

      % atoms have no punctuation in them
      c \in asString(a) => not(c = hash \/ c = colon \/ c = ques \/ c=slash);

      % Clients know how to separate the fragment from
      % the rest of the URI
      asString(p#a) = asString(asURI(p)) || {hash} || asString(a);

      % Coreference.

      % In the case of there=self, e.g. within a document,
      % two uses of a URI denote the same thing.
      % This case does *not* include XML documents that have different
      % xml:base's.
      corefer(that, that, self);

      % fragments work across documents
      corefer(asURI(p1), asURI(p2), there) => corefer(p1#a, p2#a, there);

      % a pointer to there in this document matches
      %  a pointer to the self-same document there.
      % @@perhaps this is redundant? i.e. provable from the other axioms?
      corefer(there, self, there);

      % absolute URIs corefer regardless of difference in base URI context
      % e.g. g:h =  g:h regardless of there.
      absolute(this) => corefer(this, this, there);

      %@@hmmm... authority component
      % http://foo/bar matches //foo/bar in http://anything

      % /foo/bar matches /foo/bar in /baz
      % /foo/bar matches /foo/bar in ../baz
      corefer(asURI(root1(p1)), asURI(root1(p1)), asURI(root1(p2)));
      corefer(asURI(root1(p1)), asURI(root1(p1)), asURI(parent(p2)));

      % a <~~> a    => ../a <..> a
      % ../a <..> a => ../../a <../..> a
      % and so on
      corefer(asURI(p1), asURI(p2), asURI(p3))
        => corefer(asURI(parent(p1)), asURI(parent(p2)), asURI(parent(p3)));

      %@@more?

% implies: all test cases in appendix C.

      % in C. Examples of Resolving Relative URI References,
      % the base is there, the first column is that
      % and the last column is this.
      % e.g. corefer("http://a/b/c/g", "g", "http://a/b/c/d;p?q")
      % because... @@oops... missing some axioms.
      % more general case:
      % e.g. corefer("c/g", "g", "c/d;p?q")

      % hmm... use two absolute URIs in stead of one there thingy?