% $Id: HTTP.lsl,v 1.9 2000/01/17 21:33:40 connolly Exp $

%html c.f. <br />
%html <cite><a href="http://www.w3.org/Protocols/rfc2616/rfc2616.html">Hypertext Transfer Protocol -- HTTP/1.1</a></cite> <br />
%html RFC 2616 Fielding, et al. June 1999
%html


HTTP: trait

   includes
       TTL,
       DNS,
       WebState, WebSemantics,
       ReliableTransport,
       List(Literal),
       String(HTTPFormat)
	% @@LARCHBUG: I mean a sequence of HTTPFormats indexed by
	% non-negative integers,
	% but the larch Sequence trait assumes a strict partial order
	% on E and defines things like lexicographic order. Sounds like
	% a string to me, but the larch folks call it a Sequence. Go figure.

   introduces
      http: absoluteURI, Message, Message, HTTPFormat, HTTPFormat -> Bool
        % for http(i, q, p, qf, pf) read:
	%  the message q, the request, and the message p, the reply,
	%  constitute a conforming HTTP transaction; the parsed data
	%  in the request and the reply are pf and pf respectively,
	%  and the request URI is i.

      HTTPURISchemeID: -> URISchemeID
      host: absoluteURI -> DomainName
	% e.g. host(http://www.w3.org) = www.w3.org
      port: absoluteURI -> PortNum
	% e.g. port(http://www.w3.org:8080) = 8080
	% port(http://www.w3.org) = 80
      account: absoluteURI -> AccountName
      nil: -> AccountName
        % e.g. path(http://foo@www.w3.org/index.html) = foo

        % type system of sorts...
        % hmm... @@idea for rdf-comments: does the data: URI scheme
        %          map all literals to URIs? I think so.
        % hmm... connection to XML datatypes
      hostAddr: Literal -> HostAddr
      % e.g. 207.37.25.124

      host: Channel->HostAddr
      port: Channel -> PortNum
      % if chan is a TCP endpoint, then host(chan) is
      % the IP address of the channel and port(chan) is its port


      http: Message, Message, HTTPFormat, HTTPFormat -> Bool
	    % for http(r, q, fr, fq) read: r and q are the
            % request and reply messages of a conforming HTTP transaction and
            % fr is the parsed data from r and fq is the parsed data from q.

      httpParseReqs: ByteSequence, String[HTTPFormat] -> Bool
      httpParseReps: ByteSequence,  String[HTTPFormat] -> Bool
            % for httpParseReqs(bytes, msgdatalist) read: bytes parses
            % per the HTTP grammar as a list of HTTPFormats msgdatalist.

      path: HTTPFormat -> PathName
      host: HTTPFormat -> DomainName % Host: xyx
      content: HTTPFormat -> Literal

      method: HTTPFormat -> Method
      GET: -> Method

      status: HTTPFormat -> StatusCode
      OK: -> StatusCode % 200
      NotModified: -> StatusCode % 304

      ETag: HTTPFormat -> Literal
      Last_Modified: HTTPFormat -> Literal
      If_Modified_Since: HTTPFormat -> Literal
      If_None_Match: HTTPFormat -> List[Literal]



   asserts \forall i:absoluteURI,
                   mq, mp, ma, mq2, mp2:Message,
                   reqData, repData, reqData2, repData2: HTTPFormat,
	           cmsgs, smsgs: String[HTTPFormat],
		   lit1, cbody: Literal,
		   ip1: HostAddr

        % The GET/200 OK Axiom
        % Note that it's independent of scheme(i); i.e.
	% the HTTP protocol can be used to get information about
	% ftp: URIs, or mid: URIs, etc.
        http(i, mq, mp, reqData, repData)
	/\ method(reqData) = GET
	/\ status(repData) = OK
	=> represents(mp, i, content(repData));

        % The Origin Server Axiom, TCP/IP/DNS case:
	% If you make a TCP connection to the origin server, whatever
	% it says is valid/authoritative, as long as its formatted correctly.
	i.scheme = HTTPURISchemeID
        /\ account(i) = nil   % leave http://user@host/ unspecified for now

	/\ says(ma, [URIOfDomain(host(i)), RRTypePropertyID(A), lit1])
        /\ hostAddr(lit1) = ip1
	/\ fresh(ma, mq, TTL(ma))

	/\ host(callee(conn(mq))) = ip1
	/\ port(callee(conn(mq))) = port(i)

        /\ conn(mq) = conn(mp)
	/\ idx(mq) = idx(mp)
        /\ httpParseReqs(callerBytes(conn(mq)), cmsgs)
        /\ httpParseReps(calleeBytes(conn(mp)), smsgs)

	/\ path(cmsgs[idx(mq)]) = i.path
	/\ host(cmsgs[idx(mq)]) = host(i) % HTTP 1.1-ism

	=> http(i, mq, mp, cmsgs[idx(mq)], cmsgs[idx(mp)]);


	% The Conditional GET Axiom, If_Modified_Since case
	% c.f.
%html Ari Luotonen and Kevin Altis<br />
%html <cite><a href='http://www1.cern.ch/PapersWWW94/luotonen.ps'>World-Wide Web Proxies</a></cite><br />
%html Proceedings of the 1st International WWW Conference, May 1994.
        
	http(i, mq, mp, reqData, repData)
	/\ represents(mp, i, cbody)
	/\ mp < mq2
	/\ http(i, mq2, mp2, reqData2, repData2)
	/\ method(reqData2) = GET
	/\ Last_Modified(repData) = If_Modified_Since(reqData2)
	/\ status(repData2) = NotModified
	=> represents(mp2, i, cbody);

	% The Conditional GET Axiom, If_None_Match case
	http(i, mq, mp, reqData, repData)
	/\ represents(mp, i, cbody)
	/\ mp < mq2
	/\ http(i, mq2, mp2, reqData2, repData2)
	/\ method(reqData2) = GET
	/\ ETag(repData) \in If_None_Match(reqData2) % leave * unspecified for now
	/\ status(repData2) = NotModified
	/\ ETag(repData2) = ETag(repData)
	=> represents(mp2, i, cbody); % implied metadata?